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