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