matitaB/matita/matitadaemon.ml

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