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