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 in
 218     MatitaAuthentication.set_status sid (status#set_baseuri baseuri);
 219     cgi # set_header
 220       ~cache:`No_cache
 221       ~content_type:"text/xml; charset=\"utf-8\""
 222       ();
 223     cgi#out_channel#output_string body;
 224   with
 225   | Not_found _ ->
 226     cgi # set_header
 227       ~status:`Internal_server_error
 228       ~cache:`No_cache
 229       ~content_type:"text/html; charset=\"utf-8\""
 230       ());
 231   cgi#out_channel#commit_work()
 232 ;;
 233
 234 let advance0 sid text =
 235   let status = MatitaAuthentication.get_status sid in
 236   let status = status#reset_disambiguate_db () in
 237   let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
 238        try
 239          eval_statement !include_paths (*buffer*) status (`Raw text)
 240         with
 241         | HExtlib.Localized (_,e) -> raise e
 242         (*| End_of_file -> raise Margin *)
 243      in
 244   let stringbuf = Ulexing.from_utf8_string new_statements in
 245   let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in
 246   let outstr = ref "" in
 247   ignore (SmallLexer.mk_small_printer interpr outstr stringbuf);
 248   (* prerr_endline ("parser output: " ^ !outstr); *)
 249   MatitaAuthentication.set_status sid st;
 250   parsed_len,
 251     Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
 252       () (html_of_matita !outstr), new_unparsed, st
 253
 254 let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 255   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 256   let env = cgi#environment in
 257
 258   assert (cgi#arguments <> []);
 259   let uid = cgi#argument_value "userid" in
 260   let userpw = cgi#argument_value "password" in
 261   (try
 262     MatitaAuthentication.add_user uid userpw;
 263 (*    env#set_output_header_field "Location" "/index.html" *)
 264     cgi#out_channel#output_string
 265      ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/login.html\">"
 266      ^ "</head><body>Redirecting to login page...</body></html>")
 267    with
 268    | MatitaAuthentication.UsernameCollision _ ->
 269       cgi#set_header
 270        ~cache:`No_cache
 271        ~content_type:"text/html; charset=\"utf-8\""
 272        ();
 273      cgi#out_channel#output_string
 274       "<html><head></head><body>Error: User id collision!</body></html>"
 275    | MatitaFilesystem.SvnError msg ->
 276       cgi#set_header
 277        ~cache:`No_cache
 278        ~content_type:"text/html; charset=\"utf-8\""
 279        ();
 280      cgi#out_channel#output_string
 281       ("<html><head></head><body><p>Error: Svn checkout failed!<p><p><textarea>"
 282        ^ msg ^ "</textarea></p></body></html>"));
 283   cgi#out_channel#commit_work()
 284 ;;
 285
 286 let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 287   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 288   let env = cgi#environment in
 289
 290   assert (cgi#arguments <> []);
 291   let uid = cgi#argument_value "userid" in
 292   let userpw = cgi#argument_value "password" in
 293   let pw,_ = MatitaAuthentication.lookup_user uid in
 294
 295   if pw = userpw then
 296    begin
 297     let _ = MatitaFilesystem.html_of_library uid in
 298     let sid = MatitaAuthentication.create_session uid in
 299     (* let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in
 300        cgi#set_header ~set_cookies:[cookie] (); *)
 301     env#set_output_header_field
 302       "Set-Cookie" ("session=" ^ (Uuidm.to_string sid));
 303 (*    env#set_output_header_field "Location" "/index.html" *)
 304     cgi#out_channel#output_string
 305      ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/index.html\">"
 306      ^ "</head><body>Redirecting to Matita page...</body></html>")
 307    end
 308   else
 309    begin
 310     cgi#set_header
 311       ~cache:`No_cache
 312       ~content_type:"text/html; charset=\"utf-8\""
 313       ();
 314     cgi#out_channel#output_string
 315       "<html><head></head><body>Authentication error</body></html>"
 316    end;
 317
 318   cgi#out_channel#commit_work()
 319
 320 ;;
 321
 322 let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 323   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 324   let env = cgi#environment in
 325   (try
 326     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 327     let sid = HExtlib.unopt sid in
 328     MatitaAuthentication.logout_user sid;
 329     cgi # set_header
 330       ~cache:`No_cache
 331       ~content_type:"text/html; charset=\"utf-8\""
 332       ();
 333     let text = read_file (rt_path () ^ "/logout.html") in
 334     cgi#out_channel#output_string text
 335   with
 336   | Not_found _ ->
 337     cgi # set_header
 338       ~status:`Internal_server_error
 339       ~cache:`No_cache
 340       ~content_type:"text/html; charset=\"utf-8\""
 341       ());
 342   cgi#out_channel#commit_work()
 343 ;;
 344
 345 exception File_already_exists;;
 346
 347 let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 348   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 349   let env = cgi#environment in
 350   (try
 351     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 352     let sid = HExtlib.unopt sid in
 353     let status = MatitaAuthentication.get_status sid in
 354     let uid = MatitaAuthentication.user_of_session sid in
 355     assert (cgi#arguments <> []);
 356     let locked = cgi#argument_value "locked" in
 357     let unlocked = cgi#argument_value "unlocked" in
 358     let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in
 359     let force = bool_of_string (cgi#argument_value "force") in
 360
 361     if ((not force) && (Sys.file_exists filename)) then
 362       raise File_already_exists;
 363
 364     let oc = open_out filename in
 365     output_string oc (locked ^ unlocked);
 366     close_out oc;
 367     if MatitaEngine.eos status unlocked then
 368      begin
 369       (* prerr_endline ("serializing proof objects..."); *)
 370       GrafiteTypes.Serializer.serialize
 371         ~baseuri:(NUri.uri_of_string status#baseuri) status;
 372       (* prerr_endline ("adding to the commit queue..."); *)
 373       MatitaFilesystem.add_user uid;
 374       (* prerr_endline ("done."); *)
 375      end;
 376     cgi # set_header
 377       ~cache:`No_cache
 378       ~content_type:"text/xml; charset=\"utf-8\""
 379       ();
 380     cgi#out_channel#output_string "<response>ok</response>"
 381   with
 382   | File_already_exists ->
 383       cgi#out_channel#output_string "<response>cancelled</response>"
 384   | Sys_error _ ->
 385     cgi # set_header
 386       ~status:`Internal_server_error
 387       ~cache:`No_cache
 388       ~content_type:"text/xml; charset=\"utf-8\""
 389       ());
 390   cgi#out_channel#commit_work()
 391 ;;
 392
 393 let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 394   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 395   let env = cgi#environment in
 396   (try
 397     let errors = MatitaFilesystem.do_global_commit () in
 398     prerr_endline ("commit errors: " ^ (String.concat " " errors));
 399     cgi # set_header
 400       ~cache:`No_cache
 401       ~content_type:"text/xml; charset=\"utf-8\""
 402       ();
 403     cgi#out_channel#output_string "<response>ok</response>"
 404   with
 405   | Not_found _ ->
 406     cgi # set_header
 407       ~status:`Internal_server_error
 408       ~cache:`No_cache
 409       ~content_type:"text/xml; charset=\"utf-8\""
 410       ());
 411   cgi#out_channel#commit_work()
 412 ;;
 413
 414 (* returns the length of the executed text and an html representation of the
 415  * current metasenv*)
 416 let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 417   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 418   let env = cgi#environment in
 419   (try
 420     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 421     let sid = HExtlib.unopt sid in
 422     (*
 423     cgi # set_header
 424       ~cache:`No_cache
 425       ~content_type:"text/xml; charset=\"utf-8\""
 426       ();
 427     *)
 428     let text = cgi#argument_value "body" in
 429     (* prerr_endline ("body =\n" ^ text); *)
 430     let history = MatitaAuthentication.get_history sid in
 431     let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in
 432     MatitaAuthentication.set_history sid (new_status::history);
 433     let txt = output_status new_status in
 434     let body =
 435        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
 436        new_parsed ^ "</parsed>" ^ txt
 437        ^ "</response>"
 438     in
 439     (* prerr_endline ("sending advance response:\n" ^ body); *)
 440     cgi # set_header
 441       ~cache:`No_cache
 442       ~content_type:"text/xml; charset=\"utf-8\""
 443       ();
 444     cgi#out_channel#output_string body
 445   with
 446   | Not_found _ ->
 447     cgi # set_header
 448       ~status:`Internal_server_error
 449       ~cache:`No_cache
 450       ~content_type:"text/xml; charset=\"utf-8\""
 451       ());
 452   cgi#out_channel#commit_work()
 453 ;;
 454
 455 let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 456   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 457   let env = cgi#environment in
 458   (try
 459     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 460     let sid = HExtlib.unopt sid in
 461     let history = MatitaAuthentication.get_history sid in
 462
 463     let rec aux parsed_len parsed_txt text =
 464       try
 465         prerr_endline ("evaluating: " ^ first_line text);
 466         let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in
 467         aux (parsed_len+plen) (parsed_txt ^ new_parsed) new_unparsed
 468       with
 469       | End_of_file ->
 470           let status = MatitaAuthentication.get_status sid in
 471           GrafiteTypes.Serializer.serialize
 472             ~baseuri:(NUri.uri_of_string status#baseuri) status;
 473           if parsed_len > 0 then
 474             MatitaAuthentication.set_history sid (status::history);
 475           parsed_len, parsed_txt
 476       | _ -> parsed_len, parsed_txt
 477     in
 478     (*
 479     cgi # set_header
 480       ~cache:`No_cache
 481       ~content_type:"text/xml; charset=\"utf-8\""
 482       ();
 483     *)
 484     let text = cgi#argument_value "body" in
 485     (* prerr_endline ("body =\n" ^ text); *)
 486     let parsed_len, new_parsed = aux 0 "" text in
 487     let status = MatitaAuthentication.get_status sid in
 488     let txt = output_status status in
 489     let body =
 490        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\">" ^
 491        new_parsed ^ "</parsed>" ^ txt
 492        ^ "</response>"
 493     in
 494     (*let body =
 495        "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
 496        ^ "</response>"
 497     in*)
 498     (* prerr_endline ("sending goto bottom response:\n" ^ body); *)
 499     cgi # set_header
 500       ~cache:`No_cache
 501       ~content_type:"text/xml; charset=\"utf-8\""
 502       ();
 503     cgi#out_channel#output_string body
 504    with Not_found -> cgi#set_header ~status:`Internal_server_error
 505       ~cache:`No_cache
 506       ~content_type:"text/xml; charset=\"utf-8\"" ());
 507   cgi#out_channel#commit_work()
 508 ;;
 509
 510 let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 511   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 512   let env = cgi#environment in
 513   prerr_endline "executing goto Top";
 514   (try
 515     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 516     let sid = HExtlib.unopt sid in
 517     (*
 518     cgi # set_header
 519       ~cache:`No_cache
 520       ~content_type:"text/xml; charset=\"utf-8\""
 521       ();
 522     *)
 523     let status = MatitaAuthentication.get_status sid in
 524     let uid = MatitaAuthentication.user_of_session sid in
 525     let baseuri = status#baseuri in
 526     let new_status = new MatitaEngine.status (Some uid) baseuri in
 527     NCicLibrary.time_travel new_status;
 528     let new_history = [new_status] in
 529     MatitaAuthentication.set_history sid new_history;
 530     MatitaAuthentication.set_status sid new_status;
 531     NCicLibrary.time_travel new_status;
 532     cgi # set_header
 533       ~cache:`No_cache
 534       ~content_type:"text/xml; charset=\"utf-8\""
 535       ();
 536     cgi#out_channel#output_string "<response>ok</response>"
 537    with _ ->
 538      (cgi#set_header ~status:`Internal_server_error
 539       ~cache:`No_cache
 540       ~content_type:"text/xml; charset=\"utf-8\"" ();
 541       cgi#out_channel#output_string "<response>ok</response>");
 542   cgi#out_channel#commit_work())
 543 ;;
 544
 545 let retract (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   (try
 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/xml; charset=\"utf-8\""
 555       ();
 556     *)
 557     let history = MatitaAuthentication.get_history sid in
 558     let new_history,new_status =
 559        match history with
 560          _::(status::_ as history) ->
 561           history, status
 562       | [_] -> (prerr_endline "singleton";failwith "retract")
 563       | _ -> (prerr_endline "nil"; assert false) in
 564     NCicLibrary.time_travel new_status;
 565     MatitaAuthentication.set_history sid new_history;
 566     MatitaAuthentication.set_status sid new_status;
 567     let body = output_status new_status in
 568     cgi # set_header
 569       ~cache:`No_cache
 570       ~content_type:"text/xml; charset=\"utf-8\""
 571       ();
 572     cgi#out_channel#output_string body
 573    with _ -> cgi#set_header ~status:`Internal_server_error
 574       ~cache:`No_cache
 575       ~content_type:"text/xml; charset=\"utf-8\"" ());
 576   cgi#out_channel#commit_work()
 577 ;;
 578
 579
 580 let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 581   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 582   let env = cgi#environment in
 583
 584     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
 585     let sid = HExtlib.unopt sid in
 586     (*
 587     cgi # set_header
 588       ~cache:`No_cache
 589       ~content_type:"text/html; charset=\"utf-8\""
 590       ();
 591     *)
 592     let uid = MatitaAuthentication.user_of_session sid in
 593
 594     let html = MatitaFilesystem.html_of_library uid in
 595     cgi # set_header
 596       ~cache:`No_cache
 597       ~content_type:"text/html; charset=\"utf-8\""
 598       ();
 599     cgi#out_channel#output_string
 600       ((*
 601        "<html><head>\n" ^
 602        "<title>XML Tree Control</title>\n" ^
 603        "<link href=\"treeview/xmlTree.css\" type=\"text/css\" rel=\"stylesheet\">\n" ^
 604        "<script src=\"treeview/xmlTree.js\" type=\"text/javascript\"></script>\n" ^
 605        "<body>\n" ^ *)
 606        html (* ^ "\n</body></html>" *) );
 607   cgi#out_channel#commit_work()
 608
 609 ;;
 610
 611 let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 612   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
 613   MatitaAuthentication.reset ();
 614     cgi # set_header
 615       ~cache:`No_cache
 616       ~content_type:"text/html; charset=\"utf-8\""
 617       ();
 618
 619     cgi#out_channel#output_string
 620       ("<html><head>\n" ^
 621        "<title>Matitaweb Reset</title>\n" ^
 622        "<body><H1>Reset completed</H1></body></html>");
 623     cgi#out_channel#commit_work()
 624
 625 open Netcgi1_compat.Netcgi_types;;
 626
 627 (**********************************************************************)
 628 (* Create the webserver                                               *)
 629 (**********************************************************************)
 630
 631
 632 let start() =
 633   let (opt_list, cmdline_cfg) = Netplex_main.args() in
 634
 635   let use_mt = ref true in
 636
 637   let opt_list' =
 638     [ "-mt", Arg.Set use_mt,
 639       "  Use multi-threading instead of multi-processing"
 640     ] @ opt_list in
 641
 642   Arg.parse
 643     opt_list'
 644     (fun s -> raise (Arg.Bad ("Don't know what to do with: " ^ s)))
 645     "usage: netplex [options]";
 646   let parallelizer =
 647     if !use_mt then
 648       Netplex_mt.mt()     (* multi-threading *)
 649     else
 650       Netplex_mp.mp() in  (* multi-processing *)
 651 (*
 652   let adder =
 653     { Nethttpd_services.dyn_handler = (fun _ -> process1);
 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 *)
 660   let do_advance =
 661     { Nethttpd_services.dyn_handler = (fun _ -> advance);
 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_retract =
 668     { Nethttpd_services.dyn_handler = (fun _ -> retract);
 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 goto_bottom =
 675     { Nethttpd_services.dyn_handler = (fun _ -> gotoBottom);
 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 goto_top =
 682     { Nethttpd_services.dyn_handler = (fun _ -> gotoTop);
 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 retrieve =
 689     { Nethttpd_services.dyn_handler = (fun _ -> retrieve);
 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_register =
 696     { Nethttpd_services.dyn_handler = (fun _ -> register);
 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   let do_login =
 703     { Nethttpd_services.dyn_handler = (fun _ -> login);
 704       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 705       dyn_uri = None;                 (* not needed *)
 706       dyn_translator = (fun _ -> ""); (* not needed *)
 707       dyn_accept_all_conditionals = false;
 708     } in
 709   let do_logout =
 710     { Nethttpd_services.dyn_handler = (fun _ -> logout);
 711       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 712       dyn_uri = None;                 (* not needed *)
 713       dyn_translator = (fun _ -> ""); (* not needed *)
 714       dyn_accept_all_conditionals = false;
 715     } in
 716   let do_viewlib =
 717     { Nethttpd_services.dyn_handler = (fun _ -> viewLib);
 718       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 719       dyn_uri = None;                 (* not needed *)
 720       dyn_translator = (fun _ -> ""); (* not needed *)
 721       dyn_accept_all_conditionals = false;
 722     } in
 723   let do_resetlib =
 724     { Nethttpd_services.dyn_handler = (fun _ -> resetLib);
 725       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 726       dyn_uri = None;                 (* not needed *)
 727       dyn_translator = (fun _ -> ""); (* not needed *)
 728       dyn_accept_all_conditionals = false;
 729     } in
 730   let do_save =
 731     { Nethttpd_services.dyn_handler = (fun _ -> save);
 732       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 733       dyn_uri = None;                 (* not needed *)
 734       dyn_translator = (fun _ -> ""); (* not needed *)
 735       dyn_accept_all_conditionals = false;
 736     } in
 737   let do_commit =
 738     { Nethttpd_services.dyn_handler = (fun _ -> initiate_commit);
 739       dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
 740       dyn_uri = None;                 (* not needed *)
 741       dyn_translator = (fun _ -> ""); (* not needed *)
 742       dyn_accept_all_conditionals = false;
 743     } in
 744
 745   let nethttpd_factory =
 746     Nethttpd_plex.nethttpd_factory
 747       ~handlers:[ "advance", do_advance
 748                 ; "retract", do_retract
 749                 ; "bottom", goto_bottom
 750                 ; "top", goto_top
 751                 ; "open", retrieve
 752                 ; "register", do_register
 753                 ; "login", do_login
 754                 ; "logout", do_logout
 755                 ; "reset", do_resetlib
 756                 ; "viewlib", do_viewlib
 757                 ; "save", do_save
 758                 ; "commit", do_commit]
 759       () in
 760   MatitaInit.initialize_all ();
 761   MatitaAuthentication.deserialize ();
 762   Netplex_main.startup
 763     parallelizer
 764     Netplex_log.logger_factories   (* allow all built-in logging styles *)
 765     Netplex_workload.workload_manager_factories (* ... all ways of workload management *)
 766     [ nethttpd_factory ]           (* make this nethttpd available *)
 767     cmdline_cfg
 768 ;;
 769
 770 Sys.set_signal Sys.sigpipe Sys.Signal_ignore;
 771 start();;