matitaB/matita/matitadaemon.ml

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