matitaB/matita/matitadaemon.ml

   1 open Printf;;
   2 open Http_types;;
   3
   4 module Stack = Continuationals.Stack
   5
   6 let rt_path () = Helm_registry.get "matita.rt_base_dir"
   7
   8 let libdir uid = (rt_path ()) ^ "/users/" ^ uid
   9
  10 let utf8_length = Netconversion.ustring_length `Enc_utf8
  11
  12 let mutex = Mutex.create ();;
  13
  14 let to_be_committed = ref [];;
  15
  16 (* adds a user to the commit queue; concurrent instances possible, so we
  17  * enclose the update in a CS
  18  *)
  19 let add_user_for_commit uid =
  20   Mutex.lock mutex;
  21   to_be_committed := uid::List.filter (fun x -> x <> uid) !to_be_committed;
  22   Mutex.unlock mutex;
  23 ;;
  24
  25 let do_global_commit () =
  26   prerr_endline ("to be committed: " ^ String.concat " " !to_be_committed);
  27   List.fold_left
  28     (fun out u ->
  29        let ft = MatitaAuthentication.read_ft u in
  30
  31        (* first we add new files/dirs to the repository *)
  32        let to_be_added = List.map fst
  33          (List.filter (fun (_,flag) -> flag = MatitaFilesystem.MAdd) ft)
  34        in
  35        let out =
  36          try
  37            let newout = MatitaFilesystem.add_files u to_be_added in
  38            out ^ "\n" ^ newout
  39          with
  40          | MatitaFilesystem.SvnError outstr ->
  41              prerr_endline ("ADD OF " ^ u ^ "FAILED:" ^ outstr);
  42              out
  43        in
  44
  45        (* now we update the local copy (to merge updates from other users) *)
  46        let out = try
  47          let files,anomalies,(added,conflict,del,upd,merged) =
  48            MatitaFilesystem.update_user u
  49          in
  50          let anomalies = String.concat "\n" anomalies in
  51          let details = Printf.sprintf
  52            ("%d new files\n"^^
  53             "%d deleted files\n"^^
  54             "%d updated files\n"^^
  55             "%d merged files\n"^^
  56             "%d conflicting files\n\n" ^^
  57             "Anomalies:\n%s") added del upd merged conflict anomalies
  58          in
  59          prerr_endline ("update details:\n" ^ details);
  60          MatitaAuthentication.set_file_flag u files;
  61          out ^ "\n" ^ details
  62          with
  63          | MatitaFilesystem.SvnError outstr ->
  64              prerr_endline ("UPDATE OF " ^ u ^ "FAILED:" ^ outstr);
  65              out
  66        in
  67
  68        (* we re-read the file table after updating *)
  69        let ft = MatitaAuthentication.read_ft u in
  70
  71        (* finally we perform the real commit *)
  72        let modified = (List.map fst
  73          (List.filter (fun (_,flag) -> flag = MatitaFilesystem.MModified) ft))
  74        in
  75        let to_be_committed = to_be_added @ modified
  76        in
  77        let out = try
  78          let newout = MatitaFilesystem.commit u to_be_committed in
  79          out ^ "\n" ^ newout
  80          with
  81          | MatitaFilesystem.SvnError outstr ->
  82              prerr_endline ("COMMIT OF " ^ u ^ "FAILED:" ^ outstr);
  83              out
  84        in
  85
  86        (* call stat to get the final status *)
  87        let files, anomalies = MatitaFilesystem.stat_user u in
  88        let add_count,not_added = List.fold_left
  89          (fun (ac_acc, na_acc) fname ->
  90             if List.mem fname (List.map fst files) then
  91                ac_acc, fname::na_acc
  92             else
  93                ac_acc+1, na_acc)
  94          (0,[]) to_be_added
  95        in
  96        let commit_count,not_committed = List.fold_left
  97          (fun (cc_acc, nc_acc) fname ->
  98             if List.mem fname (List.map fst files) then
  99                cc_acc, fname::nc_acc
 100             else
 101                cc_acc+1, nc_acc)
 102          (0,[]) modified
 103        in
 104        let conflicts = List.map fst (List.filter
 105          (fun (_,f) -> f = Some MatitaFilesystem.MConflict) files)
 106        in
 107        MatitaAuthentication.set_file_flag u files;
 108        out ^ "\n\n" ^ (Printf.sprintf
 109         ("COMMIT RESULTS for %s\n" ^^
 110          "==============\n" ^^
 111          "added and committed: %d of %d\n" ^^
 112          "modified and committed: %d of %d\n" ^^
 113          "not added: %s\n" ^^
 114          "not committed: %s\n" ^^
 115          "conflicts: %s\n")
 116          u add_count (List.length to_be_added) commit_count
 117          (List.length modified) (String.concat ", " not_added)
 118          (String.concat ", " not_committed) (String.concat ", " conflicts)))
 119
 120   "" (List.rev !to_be_committed)
 121 ;;
 122
 123 (*** from matitaScript.ml ***)
 124 (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *)
 125
 126 let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script *)
 127  statement
 128 =
 129   let ast,unparsed_text =
 130     match statement with
 131     | `Raw text ->
 132         (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *)
 133         let strm =
 134          GrafiteParser.parsable_statement status
 135           (Ulexing.from_utf8_string text) in
 136         let ast = MatitaEngine.get_ast status include_paths strm in
 137          ast, text
 138     | `Ast (st, text) -> st, text
 139   in
 140   let floc = match ast with
 141   | GrafiteAst.Executable (loc, _)
 142   | GrafiteAst.Comment (loc, _) -> loc in
 143
 144   let _,lend = HExtlib.loc_of_floc floc in
 145   let parsed_text, _parsed_text_len =
 146     HExtlib.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in
 147   let byte_parsed_text_len = String.length parsed_text in
 148   let unparsed_txt' =
 149     String.sub unparsed_text byte_parsed_text_len
 150       (String.length unparsed_text - byte_parsed_text_len)
 151   in
 152
 153   let status =
 154     MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
 155   in
 156   (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*)
 157     utf8_length parsed_text
 158
 159 (*let save_moo status =
 160   let script = MatitaScript.current () in
 161   let baseuri = status#baseuri in
 162   match script#bos, script#eos with
 163   | true, _ -> ()
 164   | _, true ->
 165      GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
 166       status
 167   | _ -> clean_current_baseuri status
 168 ;;*)
 169
 170 let sequent_size = ref 40;;
 171
 172 let include_paths = ref [];;
 173
 174 (* <metasenv>
 175  *   <meta number="...">
 176  *     <metaname>...</metaname>
 177  *     <goal>...</goal>
 178  *   </meta>
 179  *
 180  *   ...
 181  * </metasenv> *)
 182 let output_status s =
 183   let _,_,metasenv,subst,_ = s#obj in
 184   let render_switch = function
 185   | Stack.Open i -> "?" ^ (string_of_int i)
 186   | Stack.Closed i -> "<S>?" ^ (string_of_int i) ^ "</S>"
 187   in
 188   let int_of_switch = function
 189   | Stack.Open i | Stack.Closed i -> i
 190   in
 191   let sequent = function
 192   | Stack.Open i ->
 193       let meta = List.assoc i metasenv in
 194       snd (ApplyTransformation.ntxt_of_cic_sequent
 195         ~metasenv ~subst ~map_unicode_to_tex:false !sequent_size s (i,meta))
 196   | Stack.Closed _ -> "This goal has already been closed."
 197   in
 198   let render_sequent is_loc acc depth tag (pos,sw) =
 199     let metano = int_of_switch sw in
 200     let markup =
 201       if is_loc then
 202         (match depth, pos with
 203          | 0, 0 -> "<span class=\"activegoal\">" ^ (render_switch sw) ^ "</span>"
 204          | 0, _ ->
 205             Printf.sprintf "<span class=\"activegoal\">|<SUB>%d</SUB>: %s</span>" pos (render_switch sw)
 206          | 1, pos when Stack.head_tag s#stack = `BranchTag ->
 207              Printf.sprintf "<span class=\"passivegoal\">|<SUB>%d</SUB> : %s</span>" pos (render_switch sw)
 208          | _ -> render_switch sw)
 209       else render_switch sw
 210     in
 211     let markup =
 212       Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () markup in
 213     let markup = "<metaname>" ^ markup ^ "</metaname>" in
 214     let sequent =
 215       Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (sequent sw)
 216     in
 217     let txt0 = "<goal>" ^ sequent ^ "</goal>" in
 218     "<meta number=\"" ^ (string_of_int metano) ^ "\">" ^ markup ^
 219     txt0 ^ "</meta>" ^ acc
 220   in
 221   "<metasenv>" ^
 222     (Stack.fold
 223       ~env:(render_sequent true) ~cont:(render_sequent false)
 224       ~todo:(render_sequent false) "" s#stack) ^
 225     "</metasenv>"
 226   (* prerr_endline ("sending metasenv:\n" ^ res); res *)
 227 ;;
 228
 229 let html_of_matita s =
 230   let patt1 = Str.regexp "\005" in
 231   let patt2 = Str.regexp "\006" in
 232   let patt3 = Str.regexp "<" in
 233   let patt4 = Str.regexp ">" in
 234   let res = Str.global_replace patt4 "&gt;" s in
 235   let res = Str.global_replace patt3 "&lt;" res in
 236   let res = Str.global_replace patt2 ">" res in
 237   let res = Str.global_replace patt1 "<" res in
 238   res
 239 ;;
 240
 241 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";;
 242
 243 let first_line s =
 244   let s = Pcre.replace ~rex:heading_nl_RE s in
 245   try
 246     let nl_pos = String.index s '\n' in
 247     String.sub s 0 nl_pos
 248   with Not_found -> s
 249 ;;
 250
 251 let read_file fname =
 252   let chan = open_in fname in
 253   let lines = ref [] in
 254   (try
 255      while true do
 256        lines := input_line chan :: !lines
 257      done;
 258    with End_of_file -> close_in chan);
 259   String.concat "\n" (List.rev !lines)
 260 ;;
 261
 262 let load_index outchan =
 263   let s = read_file "index.html" in
 264   Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
 265 ;;
 266
 267 let load_doc filename outchan =
 268   let s = read_file filename in
 269   let is_png =
 270     try String.sub filename (String.length filename - 4) 4 = ".png"
 271     with Invalid_argument _ -> false
 272   in
 273   let contenttype = if is_png then "image/png" else "text/html" in
 274   Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan
 275 ;;
 276
 277 let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 278   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 279   let env = cgi#environment in
 280   (try
 281     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 282     let sid = HExtlib.unopt sid in
 283     let uid = MatitaAuthentication.user_of_session sid in
 284     (*
 285     cgi # set_header
 286       ~cache:`No_cache
 287       ~content_type:"text/xml; charset=\"utf-8\""
 288       ();
 289     *)
 290     let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in
 291     (* prerr_endline ("reading file " ^ filename); *)
 292     let body =
 293      Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false ()
 294         (html_of_matita (read_file filename)) in
 295
 296      (*   html_of_matita (read_file filename) in *)
 297     (* prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND"); *)
 298     let body = "<response><file>" ^ body ^ "</file></response>" in
 299     let baseuri, incpaths =
 300       try
 301         let root, baseuri, _fname, _tgt =
 302           Librarian.baseuri_of_script ~include_paths:[] filename in
 303         let includes =
 304          try
 305           Str.split (Str.regexp " ")
 306            (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
 307          with Not_found -> []
 308         in
 309         let rc = root :: includes in
 310          List.iter (HLog.debug) rc; baseuri, rc
 311        with
 312          Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in
 313     include_paths := incpaths;
 314     let status = (MatitaAuthentication.get_status sid)#set_baseuri baseuri in
 315     let history = [status] in
 316     MatitaAuthentication.set_status sid status;
 317     MatitaAuthentication.set_history sid history;
 318     cgi # set_header
 319       ~cache:`No_cache
 320       ~content_type:"text/xml; charset=\"utf-8\""
 321       ();
 322     cgi#out_channel#output_string body;
 323   with
 324   | Not_found _ ->
 325     cgi # set_header
 326       ~status:`Internal_server_error
 327       ~cache:`No_cache
 328       ~content_type:"text/html; charset=\"utf-8\""
 329       ());
 330   cgi#out_channel#commit_work()
 331 ;;
 332
 333 let advance0 sid text =
 334   let status = MatitaAuthentication.get_status sid in
 335   let status = status#reset_disambiguate_db () in
 336   let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
 337        try
 338          eval_statement !include_paths (*buffer*) status (`Raw text)
 339         with
 340         | HExtlib.Localized (_,e) -> raise e
 341         (*| End_of_file -> raise Margin *)
 342      in
 343   let stringbuf = Ulexing.from_utf8_string new_statements in
 344   let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in
 345   let outstr = ref "" in
 346   ignore (SmallLexer.mk_small_printer interpr outstr stringbuf);
 347   prerr_endline ("baseuri after advance = " ^ st#baseuri);
 348   (* prerr_endline ("parser output: " ^ !outstr); *)
 349   MatitaAuthentication.set_status sid st;
 350   parsed_len,
 351     Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
 352       () (html_of_matita !outstr), new_unparsed, st
 353
 354 let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 355   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 356   let _env = cgi#environment in
 357
 358   assert (cgi#arguments <> []);
 359   let uid = cgi#argument_value "userid" in
 360   let userpw = cgi#argument_value "password" in
 361   (try
 362     MatitaAuthentication.add_user uid userpw;
 363 (*    env#set_output_header_field "Location" "/index.html" *)
 364     cgi#out_channel#output_string
 365      ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/login.html\">"
 366      ^ "</head><body>Redirecting to login page...</body></html>")
 367    with
 368    | MatitaAuthentication.UsernameCollision _ ->
 369       cgi#set_header
 370        ~cache:`No_cache
 371        ~content_type:"text/html; charset=\"utf-8\""
 372        ();
 373      cgi#out_channel#output_string
 374       "<html><head></head><body>Error: User id collision!</body></html>"
 375    | MatitaFilesystem.SvnError msg ->
 376       cgi#set_header
 377        ~cache:`No_cache
 378        ~content_type:"text/html; charset=\"utf-8\""
 379        ();
 380      cgi#out_channel#output_string
 381       ("<html><head></head><body><p>Error: Svn checkout failed!<p><p><textarea>"
 382        ^ msg ^ "</textarea></p></body></html>"));
 383   cgi#out_channel#commit_work()
 384 ;;
 385
 386 let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 387   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 388   let env = cgi#environment in
 389
 390   assert (cgi#arguments <> []);
 391   let uid = cgi#argument_value "userid" in
 392   let userpw = cgi#argument_value "password" in
 393   let pw,_ = MatitaAuthentication.lookup_user uid in
 394
 395   if pw = userpw then
 396    begin
 397    let ft = MatitaAuthentication.read_ft uid in
 398    let _ = MatitaFilesystem.html_of_library uid ft in
 399     let sid = MatitaAuthentication.create_session uid in
 400     (* let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in
 401        cgi#set_header ~set_cookies:[cookie] (); *)
 402     env#set_output_header_field
 403       "Set-Cookie" ("session=" ^ (Uuidm.to_string sid));
 404 (*    env#set_output_header_field "Location" "/index.html" *)
 405     cgi#out_channel#output_string
 406      ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/index.html\">"
 407      ^ "</head><body>Redirecting to Matita page...</body></html>")
 408    end
 409   else
 410    begin
 411     cgi#set_header
 412       ~cache:`No_cache
 413       ~content_type:"text/html; charset=\"utf-8\""
 414       ();
 415     cgi#out_channel#output_string
 416       "<html><head></head><body>Authentication error</body></html>"
 417    end;
 418
 419   cgi#out_channel#commit_work()
 420
 421 ;;
 422
 423 let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 424   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 425   let env = cgi#environment in
 426   (try
 427     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 428     let sid = HExtlib.unopt sid in
 429     MatitaAuthentication.logout_user sid;
 430     cgi # set_header
 431       ~cache:`No_cache
 432       ~content_type:"text/html; charset=\"utf-8\""
 433       ();
 434     let text = read_file (rt_path () ^ "/logout.html") in
 435     cgi#out_channel#output_string text
 436   with
 437   | Not_found _ ->
 438     cgi # set_header
 439       ~status:`Internal_server_error
 440       ~cache:`No_cache
 441       ~content_type:"text/html; charset=\"utf-8\""
 442       ());
 443   cgi#out_channel#commit_work()
 444 ;;
 445
 446 exception File_already_exists;;
 447
 448 let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 449   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 450   let env = cgi#environment in
 451   (try
 452     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 453     let sid = HExtlib.unopt sid in
 454     let status = MatitaAuthentication.get_status sid in
 455     let uid = MatitaAuthentication.user_of_session sid in
 456     assert (cgi#arguments <> []);
 457     let locked = cgi#argument_value "locked" in
 458     let unlocked = cgi#argument_value "unlocked" in
 459     let dir = cgi#argument_value "dir" in
 460     let rel_filename = cgi # argument_value "file" in
 461     let filename = libdir uid ^ "/" ^ rel_filename in
 462     let force = bool_of_string (cgi#argument_value "force") in
 463     let already_exists = Sys.file_exists filename in
 464
 465     if ((not force) && already_exists) then
 466       raise File_already_exists;
 467
 468     if dir = "true" then
 469        Unix.mkdir filename 0o744
 470     else
 471      begin
 472       let oc = open_out filename in
 473       output_string oc (locked ^ unlocked);
 474       close_out oc;
 475       if MatitaEngine.eos status unlocked then
 476        begin
 477         (* prerr_endline ("serializing proof objects..."); *)
 478         GrafiteTypes.Serializer.serialize
 479           ~baseuri:(NUri.uri_of_string status#baseuri) status;
 480         (* prerr_endline ("adding to the commit queue..."); *)
 481         add_user_for_commit uid;
 482         (* prerr_endline ("done."); *)
 483        end;
 484      end;
 485     let old_flag =
 486       try
 487         List.assoc rel_filename (MatitaAuthentication.read_ft uid)
 488       with Not_found -> MatitaFilesystem.MUnversioned
 489     in
 490     if old_flag <> MatitaFilesystem.MConflict then
 491       let newflag =
 492         if already_exists then MatitaFilesystem.MModified
 493         else MatitaFilesystem.MAdd
 494       in
 495       MatitaAuthentication.set_file_flag uid [rel_filename, Some newflag];
 496     cgi # set_header
 497       ~cache:`No_cache
 498       ~content_type:"text/xml; charset=\"utf-8\""
 499       ();
 500     cgi#out_channel#output_string "<response>ok</response>"
 501   with
 502   | File_already_exists ->
 503       cgi#out_channel#output_string "<response>cancelled</response>"
 504   | Sys_error _ ->
 505     cgi # set_header
 506       ~status:`Internal_server_error
 507       ~cache:`No_cache
 508       ~content_type:"text/xml; charset=\"utf-8\""
 509       ()
 510   | e ->
 511       let estr = Printexc.to_string e in
 512       cgi#out_channel#output_string ("<response>" ^ estr ^ "</response>"));
 513   cgi#out_channel#commit_work()
 514 ;;
 515
 516 let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 517   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 518   let _env = cgi#environment in
 519   (try
 520     let out = do_global_commit () in
 521     cgi # set_header
 522       ~cache:`No_cache
 523       ~content_type:"text/xml; charset=\"utf-8\""
 524       ();
 525     cgi#out_channel#output_string "<commit>";
 526     cgi#out_channel#output_string "<response>ok</response>";
 527     cgi#out_channel#output_string ("<details>" ^ out ^ "</details>");
 528     cgi#out_channel#output_string "</commit>"
 529   with
 530   | Not_found _ ->
 531     cgi # set_header
 532       ~status:`Internal_server_error
 533       ~cache:`No_cache
 534       ~content_type:"text/xml; charset=\"utf-8\""
 535       ());
 536   cgi#out_channel#commit_work()
 537 ;;
 538
 539 let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 540   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 541   let env = cgi#environment in
 542   let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 543   let sid = HExtlib.unopt sid in
 544   let uid = MatitaAuthentication.user_of_session sid in
 545   (try
 546     let files,anomalies,(added,conflict,del,upd,merged) =
 547       MatitaFilesystem.update_user uid
 548     in
 549     let anomalies = String.concat "\n" anomalies in
 550     let details = Printf.sprintf
 551       ("%d new files\n"^^
 552        "%d deleted files\n"^^
 553        "%d updated files\n"^^
 554        "%d merged files\n"^^
 555        "%d conflicting files\n\n" ^^
 556        "Anomalies:\n%s") added del upd merged conflict anomalies
 557     in
 558     prerr_endline ("update details:\n" ^ details);
 559     let details =
 560       Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () details
 561     in
 562     MatitaAuthentication.set_file_flag uid files;
 563     cgi # set_header
 564       ~cache:`No_cache
 565       ~content_type:"text/xml; charset=\"utf-8\""
 566       ();
 567     cgi#out_channel#output_string "<update>";
 568     cgi#out_channel#output_string "<response>ok</response>";
 569     cgi#out_channel#output_string ("<details>" ^ details ^ "</details>");
 570     cgi#out_channel#output_string "</update>";
 571   with
 572   | Not_found _ ->
 573     cgi # set_header
 574       ~status:`Internal_server_error
 575       ~cache:`No_cache
 576       ~content_type:"text/xml; charset=\"utf-8\""
 577       ());
 578   cgi#out_channel#commit_work()
 579 ;;
 580
 581 (* returns the length of the executed text and an html representation of the
 582  * current metasenv*)
 583 let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 584   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 585   let env = cgi#environment in
 586   (try
 587     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 588     let sid = HExtlib.unopt sid in
 589     (*
 590     cgi # set_header
 591       ~cache:`No_cache
 592       ~content_type:"text/xml; charset=\"utf-8\""
 593       ();
 594     *)
 595     let text = cgi#argument_value "body" in
 596     (* prerr_endline ("body =\n" ^ text); *)
 597     let history = MatitaAuthentication.get_history sid in
 598     let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in
 599     MatitaAuthentication.set_history sid (new_status::history);
 600     let txt = output_status new_status in
 601     let body =
 602        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
 603        new_parsed ^ "</parsed>" ^ txt
 604        ^ "</response>"
 605     in
 606     (* prerr_endline ("sending advance response:\n" ^ body); *)
 607     cgi # set_header
 608       ~cache:`No_cache
 609       ~content_type:"text/xml; charset=\"utf-8\""
 610       ();
 611     cgi#out_channel#output_string body
 612   with
 613   | Not_found _ ->
 614     cgi # set_header
 615       ~status:`Internal_server_error
 616       ~cache:`No_cache
 617       ~content_type:"text/xml; charset=\"utf-8\""
 618       ());
 619   cgi#out_channel#commit_work()
 620 ;;
 621
 622 let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 623   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 624   let env = cgi#environment in
 625   (try
 626     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 627     let sid = HExtlib.unopt sid in
 628     let history = MatitaAuthentication.get_history sid in
 629
 630     let rec aux parsed_len parsed_txt text =
 631       try
 632         prerr_endline ("evaluating: " ^ first_line text);
 633         let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in
 634         aux (parsed_len+plen) (parsed_txt ^ new_parsed) new_unparsed
 635       with
 636       | End_of_file ->
 637           let status = MatitaAuthentication.get_status sid in
 638           GrafiteTypes.Serializer.serialize
 639             ~baseuri:(NUri.uri_of_string status#baseuri) status;
 640           if parsed_len > 0 then
 641             MatitaAuthentication.set_history sid (status::history);
 642           parsed_len, parsed_txt
 643       | _ -> parsed_len, parsed_txt
 644     in
 645     (*
 646     cgi # set_header
 647       ~cache:`No_cache
 648       ~content_type:"text/xml; charset=\"utf-8\""
 649       ();
 650     *)
 651     let text = cgi#argument_value "body" in
 652     (* prerr_endline ("body =\n" ^ text); *)
 653     let parsed_len, new_parsed = aux 0 "" text in
 654     let status = MatitaAuthentication.get_status sid in
 655     let txt = output_status status in
 656     let body =
 657        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
 658        new_parsed ^ "</parsed>" ^ txt
 659        ^ "</response>"
 660     in
 661     (*let body =
 662        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
 663        ^ "</response>"
 664     in*)
 665     (* prerr_endline ("sending goto bottom response:\n" ^ body); *)
 666     cgi # set_header
 667       ~cache:`No_cache
 668       ~content_type:"text/xml; charset=\"utf-8\""
 669       ();
 670     cgi#out_channel#output_string body
 671    with Not_found -> cgi#set_header ~status:`Internal_server_error
 672       ~cache:`No_cache
 673       ~content_type:"text/xml; charset=\"utf-8\"" ());
 674   cgi#out_channel#commit_work()
 675 ;;
 676
 677 let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 678   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 679   let env = cgi#environment in
 680   prerr_endline "executing goto Top";
 681   (try
 682     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 683     let sid = HExtlib.unopt sid in
 684     (*
 685     cgi # set_header
 686       ~cache:`No_cache
 687       ~content_type:"text/xml; charset=\"utf-8\""
 688       ();
 689     *)
 690     let status = MatitaAuthentication.get_status sid in
 691     let uid = MatitaAuthentication.user_of_session sid in
 692     let baseuri = status#baseuri in
 693     let new_status = new MatitaEngine.status (Some uid) baseuri in
 694     prerr_endline "gototop prima della time travel";
 695     NCicLibrary.time_travel new_status;
 696     prerr_endline "gototop dopo della time travel";
 697     let new_history = [new_status] in
 698     MatitaAuthentication.set_history sid new_history;
 699     MatitaAuthentication.set_status sid new_status;
 700     NCicLibrary.time_travel new_status;
 701     cgi # set_header
 702       ~cache:`No_cache
 703       ~content_type:"text/xml; charset=\"utf-8\""
 704       ();
 705     cgi#out_channel#output_string "<response>ok</response>"
 706    with _ ->
 707      (cgi#set_header ~status:`Internal_server_error
 708       ~cache:`No_cache
 709       ~content_type:"text/xml; charset=\"utf-8\"" ();
 710       cgi#out_channel#output_string "<response>ok</response>"));
 711   cgi#out_channel#commit_work()
 712 ;;
 713
 714 let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 715   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 716   let env = cgi#environment in
 717   (try
 718     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 719     let sid = HExtlib.unopt sid in
 720     (*
 721     cgi # set_header
 722       ~cache:`No_cache
 723       ~content_type:"text/xml; charset=\"utf-8\""
 724       ();
 725     *)
 726     let history = MatitaAuthentication.get_history sid in
 727     let new_history,new_status =
 728        match history with
 729          _::(status::_ as history) ->
 730           history, status
 731       | [_] -> (prerr_endline "singleton";failwith "retract")
 732       | _ -> (prerr_endline "nil"; assert false) in
 733     prerr_endline ("prima della time travel");
 734     NCicLibrary.time_travel new_status;
 735     prerr_endline ("dopo della time travel");
 736     MatitaAuthentication.set_history sid new_history;
 737     MatitaAuthentication.set_status sid new_status;
 738     prerr_endline ("baseuri after retract = " ^ new_status#baseuri);
 739     let body = output_status new_status in
 740     cgi # set_header
 741       ~cache:`No_cache
 742       ~content_type:"text/xml; charset=\"utf-8\""
 743       ();
 744     cgi#out_channel#output_string body
 745    with _ -> cgi#set_header ~status:`Internal_server_error
 746       ~cache:`No_cache
 747       ~content_type:"text/xml; charset=\"utf-8\"" ());
 748   cgi#out_channel#commit_work()
 749 ;;
 750
 751
 752 let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 753   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 754   let env = cgi#environment in
 755
 756     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 757     let sid = HExtlib.unopt sid in
 758     (*
 759     cgi # set_header
 760       ~cache:`No_cache
 761       ~content_type:"text/html; charset=\"utf-8\""
 762       ();
 763     *)
 764     let uid = MatitaAuthentication.user_of_session sid in
 765
 766     let ft = MatitaAuthentication.read_ft uid in
 767     let html = MatitaFilesystem.html_of_library uid ft in
 768     cgi # set_header
 769       ~cache:`No_cache
 770       ~content_type:"text/html; charset=\"utf-8\""
 771       ();
 772     cgi#out_channel#output_string
 773       ((*
 774        "<html><head>\n" ^
 775        "<title>XML Tree Control</title>\n" ^
 776        "<link href=\"treeview/xmlTree.css\" type=\"text/css\" rel=\"stylesheet\">\n" ^
 777        "<script src=\"treeview/xmlTree.js\" type=\"text/javascript\"></script>\n" ^
 778        "<body>\n" ^ *)
 779        html (* ^ "\n</body></html>" *) );
 780
 781     let files,anomalies = MatitaFilesystem.stat_user uid in
 782     let changed = HExtlib.filter_map
 783       (fun (n,f) -> if (f = Some MatitaFilesystem.MModified) then Some n else None) files
 784     in
 785     let changed = String.concat "\n" changed in
 786     let anomalies = String.concat "\n" anomalies in
 787     prerr_endline ("Changed:\n" ^ changed ^ "\n\nAnomalies:\n" ^ anomalies);
 788   cgi#out_channel#commit_work()
 789
 790 ;;
 791
 792 let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 793   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 794   MatitaAuthentication.reset ();
 795     cgi # set_header
 796       ~cache:`No_cache
 797       ~content_type:"text/html; charset=\"utf-8\""
 798       ();
 799
 800     cgi#out_channel#output_string
 801       ("<html><head>\n" ^
 802        "<title>Matitaweb Reset</title>\n" ^
 803        "<body><H1>Reset completed</H1></body></html>");
 804     cgi#out_channel#commit_work()
 805
 806 open Netcgi1_compat.Netcgi_types;;
 807
 808 (**********************************************************************)
 809 (* Create the webserver                                               *)
 810 (**********************************************************************)
 811
 812
 813 let start() =
 814   let (opt_list, cmdline_cfg) = Netplex_main.args() in
 815
 816   let use_mt = ref true in
 817
 818   let opt_list' =
 819     [ "-mt", Arg.Set use_mt,
 820       "  Use multi-threading instead of multi-processing"
 821     ] @ opt_list in
 822
 823   Arg.parse
 824     opt_list'
 825     (fun s -> raise (Arg.Bad ("Don't know what to do with: " ^ s)))
 826     "usage: netplex [options]";
 827   let parallelizer =
 828     if !use_mt then
 829       Netplex_mt.mt()     (* multi-threading *)
 830     else
 831       Netplex_mp.mp() in  (* multi-processing *)
 832 (*
 833   let adder =
 834     { Nethttpd_services.dyn_handler = (fun _ -> process1);
 835       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 836       dyn_uri = None;                 (* not needed *)
 837       dyn_translator = (fun _ -> ""); (* not needed *)
 838       dyn_accept_all_conditionals = false;
 839     } in
 840 *)
 841   let do_advance =
 842     { Nethttpd_services.dyn_handler = (fun _ -> advance);
 843       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 844       dyn_uri = None;                 (* not needed *)
 845       dyn_translator = (fun _ -> ""); (* not needed *)
 846       dyn_accept_all_conditionals = false;
 847     } in
 848   let do_retract =
 849     { Nethttpd_services.dyn_handler = (fun _ -> retract);
 850       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 851       dyn_uri = None;                 (* not needed *)
 852       dyn_translator = (fun _ -> ""); (* not needed *)
 853       dyn_accept_all_conditionals = false;
 854     } in
 855   let goto_bottom =
 856     { Nethttpd_services.dyn_handler = (fun _ -> gotoBottom);
 857       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 858       dyn_uri = None;                 (* not needed *)
 859       dyn_translator = (fun _ -> ""); (* not needed *)
 860       dyn_accept_all_conditionals = false;
 861     } in
 862   let goto_top =
 863     { Nethttpd_services.dyn_handler = (fun _ -> gotoTop);
 864       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 865       dyn_uri = None;                 (* not needed *)
 866       dyn_translator = (fun _ -> ""); (* not needed *)
 867       dyn_accept_all_conditionals = false;
 868     } in
 869   let retrieve =
 870     { Nethttpd_services.dyn_handler = (fun _ -> retrieve);
 871       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 872       dyn_uri = None;                 (* not needed *)
 873       dyn_translator = (fun _ -> ""); (* not needed *)
 874       dyn_accept_all_conditionals = false;
 875     } in
 876   let do_register =
 877     { Nethttpd_services.dyn_handler = (fun _ -> register);
 878       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 879       dyn_uri = None;                 (* not needed *)
 880       dyn_translator = (fun _ -> ""); (* not needed *)
 881       dyn_accept_all_conditionals = false;
 882     } in
 883   let do_login =
 884     { Nethttpd_services.dyn_handler = (fun _ -> login);
 885       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 886       dyn_uri = None;                 (* not needed *)
 887       dyn_translator = (fun _ -> ""); (* not needed *)
 888       dyn_accept_all_conditionals = false;
 889     } in
 890   let do_logout =
 891     { Nethttpd_services.dyn_handler = (fun _ -> logout);
 892       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 893       dyn_uri = None;                 (* not needed *)
 894       dyn_translator = (fun _ -> ""); (* not needed *)
 895       dyn_accept_all_conditionals = false;
 896     } in
 897   let do_viewlib =
 898     { Nethttpd_services.dyn_handler = (fun _ -> viewLib);
 899       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 900       dyn_uri = None;                 (* not needed *)
 901       dyn_translator = (fun _ -> ""); (* not needed *)
 902       dyn_accept_all_conditionals = false;
 903     } in
 904   let do_resetlib =
 905     { Nethttpd_services.dyn_handler = (fun _ -> resetLib);
 906       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 907       dyn_uri = None;                 (* not needed *)
 908       dyn_translator = (fun _ -> ""); (* not needed *)
 909       dyn_accept_all_conditionals = false;
 910     } in
 911   let do_save =
 912     { Nethttpd_services.dyn_handler = (fun _ -> save);
 913       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 914       dyn_uri = None;                 (* not needed *)
 915       dyn_translator = (fun _ -> ""); (* not needed *)
 916       dyn_accept_all_conditionals = false;
 917     } in
 918   let do_commit =
 919     { Nethttpd_services.dyn_handler = (fun _ -> initiate_commit);
 920       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 921       dyn_uri = None;                 (* not needed *)
 922       dyn_translator = (fun _ -> ""); (* not needed *)
 923       dyn_accept_all_conditionals = false;
 924     } in
 925   let do_update =
 926     { Nethttpd_services.dyn_handler = (fun _ -> svn_update);
 927       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 928       dyn_uri = None;                 (* not needed *)
 929       dyn_translator = (fun _ -> ""); (* not needed *)
 930       dyn_accept_all_conditionals = false;
 931     } in
 932
 933
 934   let nethttpd_factory =
 935     Nethttpd_plex.nethttpd_factory
 936       ~handlers:[ "advance", do_advance
 937                 ; "retract", do_retract
 938                 ; "bottom", goto_bottom
 939                 ; "top", goto_top
 940                 ; "open", retrieve
 941                 ; "register", do_register
 942                 ; "login", do_login
 943                 ; "logout", do_logout
 944                 ; "reset", do_resetlib
 945                 ; "viewlib", do_viewlib
 946                 ; "save", do_save
 947                 ; "commit", do_commit
 948                 ; "update", do_update]
 949       () in
 950   MatitaInit.initialize_all ();
 951   MatitaAuthentication.deserialize ();
 952   Netplex_main.startup
 953     parallelizer
 954     Netplex_log.logger_factories   (* allow all built-in logging styles *)
 955     Netplex_workload.workload_manager_factories (* ... all ways of workload management *)
 956     [ nethttpd_factory ]           (* make this nethttpd available *)
 957     cmdline_cfg
 958 ;;
 959
 960 Sys.set_signal Sys.sigpipe Sys.Signal_ignore;
 961 start();;