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     | NTacStatus.Error (s,None) as e ->
 367         prerr_endline
 368           ("NTacStatus.Error " ^ (Lazy.force s));
 369         raise e
 370     | NTacStatus.Error (s,Some exc) as e ->
 371         prerr_endline
 372           ("NTacStatus.Error " ^ Lazy.force s ^ " -- " ^ (Printexc.to_string exc));
 373         raise e
 374     | GrafiteDisambiguate.Ambiguous_input (loc,choices) ->
 375       let x,y = HExtlib.loc_of_floc loc in
 376       let choice_of_alias = function
 377        | GrafiteAst.Ident_alias (_,uri) -> uri, None, uri
 378        | GrafiteAst.Number_alias (None,desc)
 379        | GrafiteAst.Symbol_alias (_,None,desc) -> "cic:/fakeuri.def(1)", Some desc, desc
 380        | GrafiteAst.Number_alias (Some uri,desc)
 381        | GrafiteAst.Symbol_alias (_,Some uri,desc) -> uri, Some desc, desc
 382       in
 383       let tag_of_choice (uri,title,desc) =
 384         match title with
 385         | None -> Printf.sprintf "<choice href=\"%s\">%s</choice>"
 386             uri
 387             (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
 388         | Some t -> Printf.sprintf "<choice href=\"%s\" title=\"%s\">%s</choice>"
 389             uri
 390             (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () t)
 391             (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
 392       in
 393       let strchoices =
 394         String.concat "\n"
 395           (List.map (fun x -> tag_of_choice (choice_of_alias x)) choices)
 396       in
 397       prerr_endline (Printf.sprintf
 398         "@@@ Ambiguous input at (%d,%d). Possible choices:\n\n%s\n\n@@@ End."
 399           x y strchoices);
 400       (*
 401       let pre = Netconversion.ustring_sub `Enc_utf8  0 x text in
 402       let err = Netconversion.ustring_sub `Enc_utf8  x (y-x) text in
 403       let post = Netconversion.ustring_sub `Enc_utf8 y
 404          (Netconversion.ustring_length `Enc_utf8 text - y) text in
 405       let title = "Disambiguation Error" in
 406       (* let title = "" in *)
 407       let marked =
 408         pre ^ "\005span class=\"error\" title=\"" ^ title ^ "\"\006" ^ err ^ "\005/span\006" ^ post in
 409       let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
 410       () (html_of_matita marked) in
 411       *)
 412       let strchoices = Printf.sprintf
 413         "<ambiguity start=\"%d\" stop=\"%d\">%s</ambiguity>" x y strchoices
 414       in raise (Ambiguous strchoices)
 415    (* | End_of_file -> ...          *)
 416   in
 417   let stringbuf = Ulexing.from_utf8_string new_statements in
 418   let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in
 419   let outstr = ref "" in
 420   ignore (SmallLexer.mk_small_printer interpr outstr stringbuf);
 421   prerr_endline ("baseuri after advance = " ^ st#baseuri);
 422   (* prerr_endline ("parser output: " ^ !outstr); *)
 423   MatitaAuthentication.set_status sid st;
 424   parsed_len,
 425     Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
 426       () (html_of_matita !outstr), new_unparsed, st
 427
 428 let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 429   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 430   let _env = cgi#environment in
 431
 432   assert (cgi#arguments <> []);
 433   let uid = cgi#argument_value "userid" in
 434   let userpw = cgi#argument_value "password" in
 435   (try
 436     MatitaAuthentication.add_user uid userpw;
 437 (*    env#set_output_header_field "Location" "/index.html" *)
 438     cgi#out_channel#output_string
 439      ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/login.html\">"
 440      ^ "</head><body>Redirecting to login page...</body></html>")
 441    with
 442    | MatitaAuthentication.UsernameCollision _ ->
 443       cgi#set_header
 444        ~cache:`No_cache
 445        ~content_type:"text/html; charset=\"utf-8\""
 446        ();
 447      cgi#out_channel#output_string
 448       "<html><head></head><body>Error: User id collision!</body></html>"
 449    | MatitaFilesystem.SvnError msg ->
 450       cgi#set_header
 451        ~cache:`No_cache
 452        ~content_type:"text/html; charset=\"utf-8\""
 453        ();
 454      cgi#out_channel#output_string
 455       ("<html><head></head><body><p>Error: Svn checkout failed!<p><p><textarea>"
 456        ^ msg ^ "</textarea></p></body></html>"));
 457   cgi#out_channel#commit_work()
 458 ;;
 459
 460 let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 461   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 462   let env = cgi#environment in
 463
 464   assert (cgi#arguments <> []);
 465   let uid = cgi#argument_value "userid" in
 466   let userpw = cgi#argument_value "password" in
 467   let pw,_ = MatitaAuthentication.lookup_user uid in
 468
 469   if pw = userpw then
 470    begin
 471    let ft = MatitaAuthentication.read_ft uid in
 472    let _ = MatitaFilesystem.html_of_library uid ft in
 473     let sid = MatitaAuthentication.create_session uid in
 474     (* let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in
 475        cgi#set_header ~set_cookies:[cookie] (); *)
 476     env#set_output_header_field
 477       "Set-Cookie" ("session=" ^ (Uuidm.to_string sid));
 478 (*    env#set_output_header_field "Location" "/index.html" *)
 479     cgi#out_channel#output_string
 480      ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/index.html\">"
 481      ^ "</head><body>Redirecting to Matita page...</body></html>")
 482    end
 483   else
 484    begin
 485     cgi#set_header
 486       ~cache:`No_cache
 487       ~content_type:"text/html; charset=\"utf-8\""
 488       ();
 489     cgi#out_channel#output_string
 490       "<html><head></head><body>Authentication error</body></html>"
 491    end;
 492
 493   cgi#out_channel#commit_work()
 494
 495 ;;
 496
 497 let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 498   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 499   let env = cgi#environment in
 500   (try
 501     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 502     let sid = HExtlib.unopt sid in
 503     MatitaAuthentication.logout_user sid;
 504     cgi # set_header
 505       ~cache:`No_cache
 506       ~content_type:"text/html; charset=\"utf-8\""
 507       ();
 508     let text = read_file (rt_path () ^ "/logout.html") in
 509     cgi#out_channel#output_string text
 510   with
 511   | Not_found _ ->
 512     cgi # set_header
 513       ~status:`Internal_server_error
 514       ~cache:`No_cache
 515       ~content_type:"text/html; charset=\"utf-8\""
 516       ());
 517   cgi#out_channel#commit_work()
 518 ;;
 519
 520 exception File_already_exists;;
 521
 522 let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 523   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 524   let env = cgi#environment in
 525   (try
 526     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 527     let sid = HExtlib.unopt sid in
 528     let status = MatitaAuthentication.get_status sid in
 529     let uid = MatitaAuthentication.user_of_session sid in
 530     assert (cgi#arguments <> []);
 531     let locked = cgi#argument_value "locked" in
 532     let unlocked = cgi#argument_value "unlocked" in
 533     let dir = cgi#argument_value "dir" in
 534     let rel_filename = cgi # argument_value "file" in
 535     let filename = libdir uid ^ "/" ^ rel_filename in
 536     let force = bool_of_string (cgi#argument_value "force") in
 537     let already_exists = Sys.file_exists filename in
 538
 539     if ((not force) && already_exists) then
 540       raise File_already_exists;
 541
 542     if dir = "true" then
 543        Unix.mkdir filename 0o744
 544     else
 545      begin
 546       let oc = open_out filename in
 547       output_string oc (locked ^ unlocked);
 548       close_out oc;
 549       if MatitaEngine.eos status unlocked then
 550        begin
 551         (* prerr_endline ("serializing proof objects..."); *)
 552         GrafiteTypes.Serializer.serialize
 553           ~baseuri:(NUri.uri_of_string status#baseuri) status;
 554         (* prerr_endline ("done."); *)
 555        end;
 556      end;
 557     let old_flag =
 558       try
 559         List.assoc rel_filename (MatitaAuthentication.read_ft uid)
 560       with Not_found -> MatitaFilesystem.MUnversioned
 561     in
 562     (if old_flag <> MatitaFilesystem.MConflict &&
 563        old_flag <> MatitaFilesystem.MAdd then
 564       let newflag =
 565         if already_exists then MatitaFilesystem.MModified
 566         else MatitaFilesystem.MAdd
 567       in
 568       MatitaAuthentication.set_file_flag uid [rel_filename, Some newflag]);
 569     cgi # set_header
 570      ~cache:`No_cache
 571      ~content_type:"text/xml; charset=\"utf-8\""
 572      ();
 573     cgi#out_channel#output_string "<response>ok</response>"
 574   with
 575   | File_already_exists ->
 576       cgi#out_channel#output_string "<response>cancelled</response>"
 577   | Sys_error _ ->
 578     cgi # set_header
 579       ~status:`Internal_server_error
 580       ~cache:`No_cache
 581       ~content_type:"text/xml; charset=\"utf-8\""
 582       ()
 583   | e ->
 584       let estr = Printexc.to_string e in
 585       cgi#out_channel#output_string ("<response>" ^ estr ^ "</response>"));
 586   cgi#out_channel#commit_work()
 587 ;;
 588
 589 let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 590   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 591   let _env = cgi#environment in
 592   (try
 593     let out = do_global_commit () in
 594     cgi # set_header
 595       ~cache:`No_cache
 596       ~content_type:"text/xml; charset=\"utf-8\""
 597       ();
 598     cgi#out_channel#output_string "<commit>";
 599     cgi#out_channel#output_string "<response>ok</response>";
 600     cgi#out_channel#output_string ("<details>" ^ out ^ "</details>");
 601     cgi#out_channel#output_string "</commit>"
 602   with
 603   | Not_found _ ->
 604     cgi # set_header
 605       ~status:`Internal_server_error
 606       ~cache:`No_cache
 607       ~content_type:"text/xml; charset=\"utf-8\""
 608       ());
 609   cgi#out_channel#commit_work()
 610 ;;
 611
 612 let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 613   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 614   let env = cgi#environment in
 615   let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 616   let sid = HExtlib.unopt sid in
 617   let uid = MatitaAuthentication.user_of_session sid in
 618   (try
 619     let files,anomalies,(added,conflict,del,upd,merged) =
 620       MatitaFilesystem.update_user uid
 621     in
 622     let anomalies = String.concat "\n" anomalies in
 623     let details = Printf.sprintf
 624       ("%d new files\n"^^
 625        "%d deleted files\n"^^
 626        "%d updated files\n"^^
 627        "%d merged files\n"^^
 628        "%d conflicting files\n\n" ^^
 629        "Anomalies:\n%s") added del upd merged conflict anomalies
 630     in
 631     prerr_endline ("update details:\n" ^ details);
 632     let details =
 633       Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () details
 634     in
 635     MatitaAuthentication.set_file_flag uid files;
 636     cgi # set_header
 637       ~cache:`No_cache
 638       ~content_type:"text/xml; charset=\"utf-8\""
 639       ();
 640     cgi#out_channel#output_string "<update>";
 641     cgi#out_channel#output_string "<response>ok</response>";
 642     cgi#out_channel#output_string ("<details>" ^ details ^ "</details>");
 643     cgi#out_channel#output_string "</update>";
 644   with
 645   | Not_found _ ->
 646     cgi # set_header
 647       ~status:`Internal_server_error
 648       ~cache:`No_cache
 649       ~content_type:"text/xml; charset=\"utf-8\""
 650       ());
 651   cgi#out_channel#commit_work()
 652 ;;
 653
 654 (* returns the length of the executed text and an html representation of the
 655  * current metasenv*)
 656 let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 657   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 658   let env = cgi#environment in
 659   (try
 660     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 661     let sid = HExtlib.unopt sid in
 662     (*
 663     cgi # set_header
 664       ~cache:`No_cache
 665       ~content_type:"text/xml; charset=\"utf-8\""
 666       ();
 667     *)
 668     let text = cgi#argument_value "body" in
 669     (* prerr_endline ("body =\n" ^ text); *)
 670     let history = MatitaAuthentication.get_history sid in
 671     let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in
 672     MatitaAuthentication.set_history sid (new_status::history);
 673     let txt = output_status new_status in
 674     let body =
 675        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
 676        new_parsed ^ "</parsed>" ^ txt
 677        ^ "</response>"
 678     in
 679     (* prerr_endline ("sending advance response:\n" ^ body); *)
 680     cgi # set_header
 681       ~cache:`No_cache
 682       ~content_type:"text/xml; charset=\"utf-8\""
 683       ();
 684     cgi#out_channel#output_string body
 685    with
 686   | Emphasized_error text ->
 687 (* | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> *)
 688     let body = "<response><error>" ^ text ^ "</error></response>" in
 689     cgi # set_header
 690       ~cache:`No_cache
 691       ~content_type:"text/xml; charset=\"utf-8\""
 692       ();
 693     cgi#out_channel#output_string body
 694   | Ambiguous text ->
 695     let body = "<response>" ^ text ^ "</response>" in
 696     cgi # set_header
 697       ~cache:`No_cache
 698       ~content_type:"text/xml; charset=\"utf-8\""
 699       ();
 700     cgi#out_channel#output_string body
 701   | Not_found _ ->
 702     cgi # set_header
 703       ~status:`Internal_server_error
 704       ~cache:`No_cache
 705       ~content_type:"text/xml; charset=\"utf-8\""
 706       ());
 707   cgi#out_channel#commit_work()
 708 ;;
 709
 710 let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 711   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 712   let env = cgi#environment in
 713   (try
 714     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 715     let sid = HExtlib.unopt sid in
 716     let history = MatitaAuthentication.get_history sid in
 717
 718     let rec aux parsed_len parsed_txt text =
 719       try
 720         prerr_endline ("evaluating: " ^ first_line text);
 721         let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in
 722         aux (parsed_len+plen) (parsed_txt ^ new_parsed) new_unparsed
 723       with
 724       | End_of_file ->
 725           let status = MatitaAuthentication.get_status sid in
 726           GrafiteTypes.Serializer.serialize
 727             ~baseuri:(NUri.uri_of_string status#baseuri) status;
 728           if parsed_len > 0 then
 729             MatitaAuthentication.set_history sid (status::history);
 730           parsed_len, parsed_txt
 731       | _ -> parsed_len, parsed_txt
 732     in
 733     (*
 734     cgi # set_header
 735       ~cache:`No_cache
 736       ~content_type:"text/xml; charset=\"utf-8\""
 737       ();
 738     *)
 739     let text = cgi#argument_value "body" in
 740     (* prerr_endline ("body =\n" ^ text); *)
 741     let parsed_len, new_parsed = aux 0 "" text in
 742     let status = MatitaAuthentication.get_status sid in
 743     let txt = output_status status in
 744     let body =
 745        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
 746        new_parsed ^ "</parsed>" ^ txt
 747        ^ "</response>"
 748     in
 749     (*let body =
 750        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
 751        ^ "</response>"
 752     in*)
 753     (* prerr_endline ("sending goto bottom response:\n" ^ body); *)
 754     cgi # set_header
 755       ~cache:`No_cache
 756       ~content_type:"text/xml; charset=\"utf-8\""
 757       ();
 758     cgi#out_channel#output_string body
 759    with Not_found -> cgi#set_header ~status:`Internal_server_error
 760       ~cache:`No_cache
 761       ~content_type:"text/xml; charset=\"utf-8\"" ());
 762   cgi#out_channel#commit_work()
 763 ;;
 764
 765 let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 766   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 767   let env = cgi#environment in
 768   prerr_endline "executing goto Top";
 769   (try
 770     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 771     let sid = HExtlib.unopt sid in
 772     (*
 773     cgi # set_header
 774       ~cache:`No_cache
 775       ~content_type:"text/xml; charset=\"utf-8\""
 776       ();
 777     *)
 778     let status = MatitaAuthentication.get_status sid in
 779     let uid = MatitaAuthentication.user_of_session sid in
 780     let baseuri = status#baseuri in
 781     let new_status = new MatitaEngine.status (Some uid) baseuri in
 782     prerr_endline "gototop prima della time travel";
 783     NCicLibrary.time_travel new_status;
 784     prerr_endline "gototop dopo della time travel";
 785     let new_history = [new_status] in
 786     MatitaAuthentication.set_history sid new_history;
 787     MatitaAuthentication.set_status sid new_status;
 788     NCicLibrary.time_travel new_status;
 789     cgi # set_header
 790       ~cache:`No_cache
 791       ~content_type:"text/xml; charset=\"utf-8\""
 792       ();
 793     cgi#out_channel#output_string "<response>ok</response>"
 794    with _ ->
 795      (cgi#set_header ~status:`Internal_server_error
 796       ~cache:`No_cache
 797       ~content_type:"text/xml; charset=\"utf-8\"" ();
 798       cgi#out_channel#output_string "<response>ok</response>"));
 799   cgi#out_channel#commit_work()
 800 ;;
 801
 802 let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 803   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 804   let env = cgi#environment in
 805   (try
 806     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 807     let sid = HExtlib.unopt sid in
 808     (*
 809     cgi # set_header
 810       ~cache:`No_cache
 811       ~content_type:"text/xml; charset=\"utf-8\""
 812       ();
 813     *)
 814     let history = MatitaAuthentication.get_history sid in
 815     let new_history,new_status =
 816        match history with
 817          _::(status::_ as history) ->
 818           history, status
 819       | [_] -> (prerr_endline "singleton";failwith "retract")
 820       | _ -> (prerr_endline "nil"; assert false) in
 821     prerr_endline ("prima della time travel");
 822     NCicLibrary.time_travel new_status;
 823     prerr_endline ("dopo della time travel");
 824     MatitaAuthentication.set_history sid new_history;
 825     MatitaAuthentication.set_status sid new_status;
 826     prerr_endline ("baseuri after retract = " ^ new_status#baseuri);
 827     let body = output_status new_status in
 828     cgi # set_header
 829       ~cache:`No_cache
 830       ~content_type:"text/xml; charset=\"utf-8\""
 831       ();
 832     cgi#out_channel#output_string body
 833    with _ -> cgi#set_header ~status:`Internal_server_error
 834       ~cache:`No_cache
 835       ~content_type:"text/xml; charset=\"utf-8\"" ());
 836   cgi#out_channel#commit_work()
 837 ;;
 838
 839
 840 let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 841   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 842   let env = cgi#environment in
 843
 844     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 845     let sid = HExtlib.unopt sid in
 846     (*
 847     cgi # set_header
 848       ~cache:`No_cache
 849       ~content_type:"text/html; charset=\"utf-8\""
 850       ();
 851     *)
 852     let uid = MatitaAuthentication.user_of_session sid in
 853
 854     let ft = MatitaAuthentication.read_ft uid in
 855     let html = MatitaFilesystem.html_of_library uid ft in
 856     cgi # set_header
 857       ~cache:`No_cache
 858       ~content_type:"text/html; charset=\"utf-8\""
 859       ();
 860     cgi#out_channel#output_string
 861       ((*
 862        "<html><head>\n" ^
 863        "<title>XML Tree Control</title>\n" ^
 864        "<link href=\"treeview/xmlTree.css\" type=\"text/css\" rel=\"stylesheet\">\n" ^
 865        "<script src=\"treeview/xmlTree.js\" type=\"text/javascript\"></script>\n" ^
 866        "<body>\n" ^ *)
 867        html (* ^ "\n</body></html>" *) );
 868
 869     let files,anomalies = MatitaFilesystem.stat_user uid in
 870     let changed = HExtlib.filter_map
 871       (fun (n,f) -> if (f = Some MatitaFilesystem.MModified) then Some n else None) files
 872     in
 873     let changed = String.concat "\n" changed in
 874     let anomalies = String.concat "\n" anomalies in
 875     prerr_endline ("Changed:\n" ^ changed ^ "\n\nAnomalies:\n" ^ anomalies);
 876   cgi#out_channel#commit_work()
 877
 878 ;;
 879
 880 let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 881   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 882   MatitaAuthentication.reset ();
 883     cgi # set_header
 884       ~cache:`No_cache
 885       ~content_type:"text/html; charset=\"utf-8\""
 886       ();
 887
 888     cgi#out_channel#output_string
 889       ("<html><head>\n" ^
 890        "<title>Matitaweb Reset</title>\n" ^
 891        "<body><H1>Reset completed</H1></body></html>");
 892     cgi#out_channel#commit_work()
 893
 894 open Netcgi1_compat.Netcgi_types;;
 895
 896 (**********************************************************************)
 897 (* Create the webserver                                               *)
 898 (**********************************************************************)
 899
 900
 901 let start() =
 902   let (opt_list, cmdline_cfg) = Netplex_main.args() in
 903
 904   let use_mt = ref true in
 905
 906   let opt_list' =
 907     [ "-mt", Arg.Set use_mt,
 908       "  Use multi-threading instead of multi-processing"
 909     ] @ opt_list in
 910
 911   Arg.parse
 912     opt_list'
 913     (fun s -> raise (Arg.Bad ("Don't know what to do with: " ^ s)))
 914     "usage: netplex [options]";
 915   let parallelizer =
 916     if !use_mt then
 917       Netplex_mt.mt()     (* multi-threading *)
 918     else
 919       Netplex_mp.mp() in  (* multi-processing *)
 920 (*
 921   let adder =
 922     { Nethttpd_services.dyn_handler = (fun _ -> process1);
 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 *)
 929   let do_advance =
 930     { Nethttpd_services.dyn_handler = (fun _ -> advance);
 931       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 932       dyn_uri = None;                 (* not needed *)
 933       dyn_translator = (fun _ -> ""); (* not needed *)
 934       dyn_accept_all_conditionals = false;
 935     } in
 936   let do_retract =
 937     { Nethttpd_services.dyn_handler = (fun _ -> retract);
 938       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 939       dyn_uri = None;                 (* not needed *)
 940       dyn_translator = (fun _ -> ""); (* not needed *)
 941       dyn_accept_all_conditionals = false;
 942     } in
 943   let goto_bottom =
 944     { Nethttpd_services.dyn_handler = (fun _ -> gotoBottom);
 945       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 946       dyn_uri = None;                 (* not needed *)
 947       dyn_translator = (fun _ -> ""); (* not needed *)
 948       dyn_accept_all_conditionals = false;
 949     } in
 950   let goto_top =
 951     { Nethttpd_services.dyn_handler = (fun _ -> gotoTop);
 952       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 953       dyn_uri = None;                 (* not needed *)
 954       dyn_translator = (fun _ -> ""); (* not needed *)
 955       dyn_accept_all_conditionals = false;
 956     } in
 957   let retrieve =
 958     { Nethttpd_services.dyn_handler = (fun _ -> retrieve);
 959       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 960       dyn_uri = None;                 (* not needed *)
 961       dyn_translator = (fun _ -> ""); (* not needed *)
 962       dyn_accept_all_conditionals = false;
 963     } in
 964   let do_register =
 965     { Nethttpd_services.dyn_handler = (fun _ -> register);
 966       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 967       dyn_uri = None;                 (* not needed *)
 968       dyn_translator = (fun _ -> ""); (* not needed *)
 969       dyn_accept_all_conditionals = false;
 970     } in
 971   let do_login =
 972     { Nethttpd_services.dyn_handler = (fun _ -> login);
 973       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 974       dyn_uri = None;                 (* not needed *)
 975       dyn_translator = (fun _ -> ""); (* not needed *)
 976       dyn_accept_all_conditionals = false;
 977     } in
 978   let do_logout =
 979     { Nethttpd_services.dyn_handler = (fun _ -> logout);
 980       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 981       dyn_uri = None;                 (* not needed *)
 982       dyn_translator = (fun _ -> ""); (* not needed *)
 983       dyn_accept_all_conditionals = false;
 984     } in
 985   let do_viewlib =
 986     { Nethttpd_services.dyn_handler = (fun _ -> viewLib);
 987       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 988       dyn_uri = None;                 (* not needed *)
 989       dyn_translator = (fun _ -> ""); (* not needed *)
 990       dyn_accept_all_conditionals = false;
 991     } in
 992   let do_resetlib =
 993     { Nethttpd_services.dyn_handler = (fun _ -> resetLib);
 994       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 995       dyn_uri = None;                 (* not needed *)
 996       dyn_translator = (fun _ -> ""); (* not needed *)
 997       dyn_accept_all_conditionals = false;
 998     } in
 999   let do_save =
1000     { Nethttpd_services.dyn_handler = (fun _ -> save);
1001       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
1002       dyn_uri = None;                 (* not needed *)
1003       dyn_translator = (fun _ -> ""); (* not needed *)
1004       dyn_accept_all_conditionals = false;
1005     } in
1006   let do_commit =
1007     { Nethttpd_services.dyn_handler = (fun _ -> initiate_commit);
1008       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
1009       dyn_uri = None;                 (* not needed *)
1010       dyn_translator = (fun _ -> ""); (* not needed *)
1011       dyn_accept_all_conditionals = false;
1012     } in
1013   let do_update =
1014     { Nethttpd_services.dyn_handler = (fun _ -> svn_update);
1015       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
1016       dyn_uri = None;                 (* not needed *)
1017       dyn_translator = (fun _ -> ""); (* not needed *)
1018       dyn_accept_all_conditionals = false;
1019     } in
1020
1021
1022   let nethttpd_factory =
1023     Nethttpd_plex.nethttpd_factory
1024       ~handlers:[ "advance", do_advance
1025                 ; "retract", do_retract
1026                 ; "bottom", goto_bottom
1027                 ; "top", goto_top
1028                 ; "open", retrieve
1029                 ; "register", do_register
1030                 ; "login", do_login
1031                 ; "logout", do_logout
1032                 ; "reset", do_resetlib
1033                 ; "viewlib", do_viewlib
1034                 ; "save", do_save
1035                 ; "commit", do_commit
1036                 ; "update", do_update]
1037       () in
1038   MatitaInit.initialize_all ();
1039   MatitaAuthentication.deserialize ();
1040   Netplex_main.startup
1041     parallelizer
1042     Netplex_log.logger_factories   (* allow all built-in logging styles *)
1043     Netplex_workload.workload_manager_factories (* ... all ways of workload management *)
1044     [ nethttpd_factory ]           (* make this nethttpd available *)
1045     cmdline_cfg
1046 ;;
1047
1048 Sys.set_signal Sys.sigpipe Sys.Signal_ignore;
1049 start();;