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    with
 273    | MatitaAuthentication.UsernameCollision _ ->
 274       cgi#set_header
 275        ~cache:`No_cache
 276        ~content_type:"text/html; charset=\"utf-8\""
 277        ();
 278      cgi#out_channel#output_string
 279       "<html><head></head><body>Error: User id collision!</body></html>"
 280    | MatitaFilesystem.SvnError msg ->
 281       cgi#set_header
 282        ~cache:`No_cache
 283        ~content_type:"text/html; charset=\"utf-8\""
 284        ();
 285      cgi#out_channel#output_string
 286       ("<html><head></head><body><p>Error: Svn checkout failed!<p><p><textarea>"
 287        ^ msg ^ "</textarea></p></body></html>"));
 288   cgi#out_channel#commit_work()
 289 ;;
 290
 291 let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 292   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 293   let env = cgi#environment in
 294
 295   assert (cgi#arguments <> []);
 296   let uid = cgi#argument_value "userid" in
 297   let userpw = cgi#argument_value "password" in
 298   let pw,_ = MatitaAuthentication.lookup_user uid in
 299
 300   if pw = userpw then
 301    begin
 302     let _ = MatitaFilesystem.html_of_library uid in
 303     let sid = MatitaAuthentication.create_session uid in
 304     (* let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in
 305        cgi#set_header ~set_cookies:[cookie] (); *)
 306     env#set_output_header_field
 307       "Set-Cookie" ("session=" ^ (Uuidm.to_string sid));
 308     env#set_output_header_field "Location" "/index.html"
 309    end
 310   else
 311    begin
 312     prerr_endline ("ERROR: received " ^ userpw ^ "but the password is " ^ pw);
 313     cgi#set_header
 314       ~cache:`No_cache
 315       ~content_type:"text/html; charset=\"utf-8\""
 316       ();
 317     cgi#out_channel#output_string
 318       "<html><head></head><body>Authentication error</body></html>"
 319    end;
 320
 321   cgi#out_channel#commit_work()
 322
 323 ;;
 324
 325 let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 326   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 327   let env = cgi#environment in
 328   (try
 329     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 330     let sid = HExtlib.unopt sid in
 331     MatitaAuthentication.logout_user sid;
 332     cgi # set_header
 333       ~cache:`No_cache
 334       ~content_type:"text/html; charset=\"utf-8\""
 335       ();
 336     let text = read_file (rt_path () ^ "/logout.html") in
 337     cgi#out_channel#output_string text
 338   with
 339   | Not_found _ ->
 340     cgi # set_header
 341       ~status:`Internal_server_error
 342       ~cache:`No_cache
 343       ~content_type:"text/html; charset=\"utf-8\""
 344       ());
 345   cgi#out_channel#commit_work()
 346 ;;
 347
 348 let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 349   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 350   let env = cgi#environment in
 351   (try
 352     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 353     let sid = HExtlib.unopt sid in
 354     let status = MatitaAuthentication.get_status sid in
 355     let uid = MatitaAuthentication.user_of_session sid in
 356     assert (cgi#arguments <> []);
 357     let locked = cgi#argument_value "locked" in
 358     let unlocked = cgi#argument_value "unlocked" in
 359     let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in
 360     prerr_endline ("Matita will save the file for user " ^ uid);
 361     let oc = open_out filename in
 362     output_string oc (locked ^ unlocked);
 363     close_out oc;
 364     if MatitaEngine.eos status unlocked then
 365      begin
 366       prerr_endline ("serializing proof objects...");
 367       GrafiteTypes.Serializer.serialize
 368         ~baseuri:(NUri.uri_of_string status#baseuri) status;
 369       prerr_endline ("adding to the commit queue...");
 370       MatitaFilesystem.add_user uid;
 371       prerr_endline ("done.");
 372      end;
 373     cgi # set_header
 374       ~cache:`No_cache
 375       ~content_type:"text/xml; charset=\"utf-8\""
 376       ();
 377     cgi#out_channel#output_string "<response>ok</response>"
 378   with
 379   | Not_found _ ->
 380     cgi # set_header
 381       ~status:`Internal_server_error
 382       ~cache:`No_cache
 383       ~content_type:"text/xml; charset=\"utf-8\""
 384       ());
 385   cgi#out_channel#commit_work()
 386 ;;
 387
 388 let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 389   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 390   let env = cgi#environment in
 391   (try
 392     let errors = MatitaFilesystem.do_global_commit () in
 393     prerr_endline ("commit errors: " ^ (String.concat " " errors));
 394     cgi # set_header
 395       ~cache:`No_cache
 396       ~content_type:"text/xml; charset=\"utf-8\""
 397       ();
 398     cgi#out_channel#output_string "<response>ok</response>"
 399   with
 400   | Not_found _ ->
 401     cgi # set_header
 402       ~status:`Internal_server_error
 403       ~cache:`No_cache
 404       ~content_type:"text/xml; charset=\"utf-8\""
 405       ());
 406   cgi#out_channel#commit_work()
 407 ;;
 408
 409 (* returns the length of the executed text and an html representation of the
 410  * current metasenv*)
 411 let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 412   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 413   let env = cgi#environment in
 414   (try
 415     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 416     let sid = HExtlib.unopt sid in
 417     (*
 418     cgi # set_header
 419       ~cache:`No_cache
 420       ~content_type:"text/xml; charset=\"utf-8\""
 421       ();
 422     *)
 423     let text = cgi#argument_value "body" in
 424     prerr_endline ("body =\n" ^ text);
 425     let history = MatitaAuthentication.get_history sid in
 426     let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in
 427     MatitaAuthentication.set_history sid (new_status::history);
 428     let txt = output_status new_status in
 429     let body =
 430        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
 431        new_parsed ^ "</parsed>" ^ txt
 432        ^ "</response>"
 433     in
 434     prerr_endline ("sending advance response:\n" ^ body);
 435     cgi # set_header
 436       ~cache:`No_cache
 437       ~content_type:"text/xml; charset=\"utf-8\""
 438       ();
 439     cgi#out_channel#output_string body
 440   with
 441   | Not_found _ ->
 442     cgi # set_header
 443       ~status:`Internal_server_error
 444       ~cache:`No_cache
 445       ~content_type:"text/xml; charset=\"utf-8\""
 446       ());
 447   cgi#out_channel#commit_work()
 448 ;;
 449
 450 let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 451   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 452   let env = cgi#environment in
 453   (try
 454     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 455     let sid = HExtlib.unopt sid in
 456     let history = MatitaAuthentication.get_history sid in
 457
 458     let rec aux parsed_len parsed_txt text =
 459       try
 460         prerr_endline ("evaluating: " ^ first_line text);
 461         let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in
 462         aux (parsed_len+plen) (parsed_txt ^ new_parsed) new_unparsed
 463       with
 464       | End_of_file ->
 465           let status = MatitaAuthentication.get_status sid in
 466           GrafiteTypes.Serializer.serialize
 467             ~baseuri:(NUri.uri_of_string status#baseuri) status;
 468           if parsed_len > 0 then
 469             MatitaAuthentication.set_history sid (status::history);
 470           parsed_len, parsed_txt
 471       | _ -> parsed_len, parsed_txt
 472     in
 473     (*
 474     cgi # set_header
 475       ~cache:`No_cache
 476       ~content_type:"text/xml; charset=\"utf-8\""
 477       ();
 478     *)
 479     let text = cgi#argument_value "body" in
 480     prerr_endline ("body =\n" ^ text);
 481     let parsed_len, new_parsed = aux 0 "" text in
 482     let status = MatitaAuthentication.get_status sid in
 483     let txt = output_status status in
 484     let body =
 485        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
 486        new_parsed ^ "</parsed>" ^ txt
 487        ^ "</response>"
 488     in
 489     (*let body =
 490        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
 491        ^ "</response>"
 492     in*)
 493     prerr_endline ("sending goto bottom response:\n" ^ body);
 494     cgi # set_header
 495       ~cache:`No_cache
 496       ~content_type:"text/xml; charset=\"utf-8\""
 497       ();
 498     cgi#out_channel#output_string body
 499    with Not_found -> cgi#set_header ~status:`Internal_server_error
 500       ~cache:`No_cache
 501       ~content_type:"text/xml; charset=\"utf-8\"" ());
 502   cgi#out_channel#commit_work()
 503 ;;
 504
 505 let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 506   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 507   let env = cgi#environment in
 508   prerr_endline "executing retract";
 509   (try
 510     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 511     let sid = HExtlib.unopt sid in
 512     (*
 513     cgi # set_header
 514       ~cache:`No_cache
 515       ~content_type:"text/xml; charset=\"utf-8\""
 516       ();
 517     *)
 518     let history = MatitaAuthentication.get_history sid in
 519     let new_history,new_status =
 520        match history with
 521          _::(status::_ as history) ->
 522           history, status
 523       | [_] -> (prerr_endline "singleton";failwith "retract")
 524       | _ -> (prerr_endline "nil"; assert false) in
 525     prerr_endline "before time_travel";
 526     NCicLibrary.time_travel new_status;
 527     prerr_endline "after time travel";
 528     MatitaAuthentication.set_history sid new_history;
 529     MatitaAuthentication.set_status sid new_status;
 530     prerr_endline ("after retract history.length = " ^
 531       string_of_int (List.length new_history));
 532     let body = output_status new_status in
 533     cgi # set_header
 534       ~cache:`No_cache
 535       ~content_type:"text/xml; charset=\"utf-8\""
 536       ();
 537     cgi#out_channel#output_string body
 538    with _ -> cgi#set_header ~status:`Internal_server_error
 539       ~cache:`No_cache
 540       ~content_type:"text/xml; charset=\"utf-8\"" ());
 541   cgi#out_channel#commit_work()
 542 ;;
 543
 544
 545 let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 546   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 547   let env = cgi#environment in
 548
 549     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 550     let sid = HExtlib.unopt sid in
 551     (*
 552     cgi # set_header
 553       ~cache:`No_cache
 554       ~content_type:"text/html; charset=\"utf-8\""
 555       ();
 556     *)
 557     let uid = MatitaAuthentication.user_of_session sid in
 558
 559     let html = MatitaFilesystem.html_of_library uid in
 560     cgi # set_header
 561       ~cache:`No_cache
 562       ~content_type:"text/html; charset=\"utf-8\""
 563       ();
 564     cgi#out_channel#output_string
 565       ((*
 566        "<html><head>\n" ^
 567        "<title>XML Tree Control</title>\n" ^
 568        "<link href=\"treeview/xmlTree.css\" type=\"text/css\" rel=\"stylesheet\">\n" ^
 569        "<script src=\"treeview/xmlTree.js\" type=\"text/javascript\"></script>\n" ^
 570        "<body>\n" ^ *)
 571        html (* ^ "\n</body></html>" *) );
 572   cgi#out_channel#commit_work()
 573
 574 ;;
 575
 576 let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 577   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 578   MatitaAuthentication.reset ();
 579     cgi # set_header
 580       ~cache:`No_cache
 581       ~content_type:"text/html; charset=\"utf-8\""
 582       ();
 583
 584     cgi#out_channel#output_string
 585       ("<html><head>\n" ^
 586        "<title>Matitaweb Reset</title>\n" ^
 587        "<body><H1>Reset completed</H1></body></html>");
 588     cgi#out_channel#commit_work()
 589
 590 open Netcgi1_compat.Netcgi_types;;
 591
 592 (**********************************************************************)
 593 (* Create the webserver                                               *)
 594 (**********************************************************************)
 595
 596
 597 let start() =
 598   let (opt_list, cmdline_cfg) = Netplex_main.args() in
 599
 600   let use_mt = ref true in
 601
 602   let opt_list' =
 603     [ "-mt", Arg.Set use_mt,
 604       "  Use multi-threading instead of multi-processing"
 605     ] @ opt_list in
 606
 607   Arg.parse
 608     opt_list'
 609     (fun s -> raise (Arg.Bad ("Don't know what to do with: " ^ s)))
 610     "usage: netplex [options]";
 611   let parallelizer =
 612     if !use_mt then
 613       Netplex_mt.mt()     (* multi-threading *)
 614     else
 615       Netplex_mp.mp() in  (* multi-processing *)
 616 (*
 617   let adder =
 618     { Nethttpd_services.dyn_handler = (fun _ -> process1);
 619       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 620       dyn_uri = None;                 (* not needed *)
 621       dyn_translator = (fun _ -> ""); (* not needed *)
 622       dyn_accept_all_conditionals = false;
 623     } in
 624 *)
 625   let do_advance =
 626     { Nethttpd_services.dyn_handler = (fun _ -> advance);
 627       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 628       dyn_uri = None;                 (* not needed *)
 629       dyn_translator = (fun _ -> ""); (* not needed *)
 630       dyn_accept_all_conditionals = false;
 631     } in
 632   let do_retract =
 633     { Nethttpd_services.dyn_handler = (fun _ -> retract);
 634       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 635       dyn_uri = None;                 (* not needed *)
 636       dyn_translator = (fun _ -> ""); (* not needed *)
 637       dyn_accept_all_conditionals = false;
 638     } in
 639   let goto_bottom =
 640     { Nethttpd_services.dyn_handler = (fun _ -> gotoBottom);
 641       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 642       dyn_uri = None;                 (* not needed *)
 643       dyn_translator = (fun _ -> ""); (* not needed *)
 644       dyn_accept_all_conditionals = false;
 645     } in
 646   let retrieve =
 647     { Nethttpd_services.dyn_handler = (fun _ -> retrieve);
 648       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 649       dyn_uri = None;                 (* not needed *)
 650       dyn_translator = (fun _ -> ""); (* not needed *)
 651       dyn_accept_all_conditionals = false;
 652     } in
 653   let do_register =
 654     { Nethttpd_services.dyn_handler = (fun _ -> register);
 655       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 656       dyn_uri = None;                 (* not needed *)
 657       dyn_translator = (fun _ -> ""); (* not needed *)
 658       dyn_accept_all_conditionals = false;
 659     } in
 660   let do_login =
 661     { Nethttpd_services.dyn_handler = (fun _ -> login);
 662       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 663       dyn_uri = None;                 (* not needed *)
 664       dyn_translator = (fun _ -> ""); (* not needed *)
 665       dyn_accept_all_conditionals = false;
 666     } in
 667   let do_logout =
 668     { Nethttpd_services.dyn_handler = (fun _ -> logout);
 669       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 670       dyn_uri = None;                 (* not needed *)
 671       dyn_translator = (fun _ -> ""); (* not needed *)
 672       dyn_accept_all_conditionals = false;
 673     } in
 674   let do_viewlib =
 675     { Nethttpd_services.dyn_handler = (fun _ -> viewLib);
 676       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 677       dyn_uri = None;                 (* not needed *)
 678       dyn_translator = (fun _ -> ""); (* not needed *)
 679       dyn_accept_all_conditionals = false;
 680     } in
 681   let do_resetlib =
 682     { Nethttpd_services.dyn_handler = (fun _ -> resetLib);
 683       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 684       dyn_uri = None;                 (* not needed *)
 685       dyn_translator = (fun _ -> ""); (* not needed *)
 686       dyn_accept_all_conditionals = false;
 687     } in
 688   let do_save =
 689     { Nethttpd_services.dyn_handler = (fun _ -> save);
 690       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 691       dyn_uri = None;                 (* not needed *)
 692       dyn_translator = (fun _ -> ""); (* not needed *)
 693       dyn_accept_all_conditionals = false;
 694     } in
 695   let do_commit =
 696     { Nethttpd_services.dyn_handler = (fun _ -> initiate_commit);
 697       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 698       dyn_uri = None;                 (* not needed *)
 699       dyn_translator = (fun _ -> ""); (* not needed *)
 700       dyn_accept_all_conditionals = false;
 701     } in
 702
 703   let nethttpd_factory =
 704     Nethttpd_plex.nethttpd_factory
 705       ~handlers:[ "advance", do_advance
 706                 ; "retract", do_retract
 707                 ; "bottom", goto_bottom
 708                 ; "open", retrieve
 709                 ; "register", do_register
 710                 ; "login", do_login
 711                 ; "logout", do_logout
 712                 ; "reset", do_resetlib
 713                 ; "viewlib", do_viewlib
 714                 ; "save", do_save
 715                 ; "commit", do_commit]
 716       () in
 717   MatitaInit.initialize_all ();
 718   MatitaAuthentication.deserialize ();
 719   Netplex_main.startup
 720     parallelizer
 721     Netplex_log.logger_factories   (* allow all built-in logging styles *)
 722     Netplex_workload.workload_manager_factories (* ... all ways of workload management *)
 723     [ nethttpd_factory ]           (* make this nethttpd available *)
 724     cmdline_cfg
 725 ;;
 726
 727 Sys.set_signal Sys.sigpipe Sys.Signal_ignore;
 728 start();;