matitaB/matita/matitadaemon.ml

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