Multi-user matita: changed the status object to include a ``user'' method

[helm.git] / matitaB / matita / matitadaemon.ml

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 65ddaf2cc4e3cce064ed1e6e54920cf1f0ee44a3..8dbfa45112cc9be7074e37969fe5bdd7f4d83dc8 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -5,6 +5,12 @@ module Stack = Continuationals.Stack
 
 let utf8_length = Netconversion.ustring_length `Enc_utf8
 
+let utf8_parsed_text s floc =
+  let start, stop = HExtlib.loc_of_floc floc in
+  let len = stop - start in
+  let res = Netconversion.ustring_sub `Enc_utf8 start len s in
+  res, String.length res
+
 (*** from matitaScript.ml ***)
 (* let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" *)
 
@@ -27,8 +33,8 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script
   | GrafiteAst.Comment (loc, _) -> loc in
   
   let _,lend = HExtlib.loc_of_floc floc in 
-  let parsed_text, parsed_text_len = 
-    MatitaGtkMisc.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in
+  let parsed_text, _parsed_text_len = 
+    utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in
   let byte_parsed_text_len = String.length parsed_text in
   let unparsed_txt' = 
     String.sub unparsed_text byte_parsed_text_len 
@@ -41,11 +47,12 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script
   (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*)
     utf8_length parsed_text
 
-
-let status = ref (new MatitaEngine.status "cic:/matita");;
+(* FIXME: currently hard coded to single user mode *)
+let status = ref (new MatitaEngine.status (Some "ricciott") "cic:/matita");;
 let history = ref [!status];;
+let sequent_size = ref 40;;
 
-let include_paths = ["/home/barolo/matitaB/matita/lib"];;
+let include_paths = ref [];;
 
 (* <metasenv>
  *   <meta number="...">
@@ -68,7 +75,7 @@ let output_status s =
   | Stack.Open i ->
       let meta = List.assoc i metasenv in
       snd (ApplyTransformation.ntxt_of_cic_sequent 
-        ~metasenv ~subst ~map_unicode_to_tex:false 80 s (i,meta))
+        ~metasenv ~subst ~map_unicode_to_tex:false !sequent_size s (i,meta))
   | Stack.Closed _ -> "This goal has already been closed."
   in
   let render_sequent is_loc acc depth tag (pos,sw) =
@@ -155,20 +162,6 @@ let load_doc filename outchan =
   Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan
 ;;
 
-let call_service outchan =
-  try 
-   (ignore(MatitaEngine.assert_ng 
-     ~include_paths:["/home/barolo/matitaB/matita/lib"] (* ~outch:outchan *)
-    "/home/barolo/matitaB/matita/lib/basics/pts.ma");
-    prerr_endline "fatto";
-    let s = read_file "/home/barolo/matitaB/matita/lib/basics/pts.ma.mad"
-    in
-    Http_daemon.respond ~headers:["Content-Type", "text/html"] ~code:(`Code 200) ~body:s outchan
-   )
-  with
-  e -> Http_daemon.respond ~code:(`Code 500) outchan
-;;
-
 let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   cgi # set_header 
@@ -182,9 +175,21 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
       (read_file filename) in
   prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND");
   let body = "<file>" ^ body ^ "</file>" in
-  let _,baseuri,_,_ = 
-    Librarian.baseuri_of_script ~include_paths:[] filename
-  in
+  let baseuri, incpaths = 
+    try 
+      let root, baseuri, _fname, _tgt = 
+        Librarian.baseuri_of_script ~include_paths:[] filename in 
+      let includes =
+       try
+        Str.split (Str.regexp " ") 
+         (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+       with Not_found -> []
+      in
+      let rc = root :: includes in
+       List.iter (HLog.debug) rc; baseuri, rc
+     with 
+       Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in
+  include_paths := incpaths;
   status := (!status)#set_baseuri baseuri;
   cgi#out_channel#output_string body;
   cgi#out_channel#commit_work()
@@ -193,11 +198,12 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 let advance0 text =
   let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
        (* try *)
-         eval_statement include_paths (*buffer*) !status (`Raw text)
+         eval_statement !include_paths (*buffer*) !status (`Raw text)
        (* with End_of_file -> raise Margin *)
      in
   status := st;
   history := st :: !history;
+  prerr_endline ("after advance0 history.length = " ^ string_of_int (List.length !history));
   parsed_len, new_unparsed
 
 
@@ -261,9 +267,10 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
         history, status
     | [_] -> (prerr_endline "singleton";failwith "retract")
     | _ -> (prerr_endline "nil"; assert false) in
-  NCicLibrary.time_travel !status;
+  NCicLibrary.time_travel new_status;
   history := new_history;
   status := new_status;
+  prerr_endline ("after retract history.length = " ^ string_of_int (List.length !history));
   let body = output_status !status in
   cgi#out_channel#output_string body;
   cgi#out_channel#commit_work() 
@@ -342,6 +349,10 @@ let start() =
                 ; "open", retrieve ]
       () in
   MatitaInit.initialize_all ();
+  (* test begin *)
+  MatitaAuthentication.add_user "ricciott" "pippo123";
+  MatitaAuthentication.add_user "asperti" "pluto456";
+  (* test end *)
   Netplex_main.startup
     parallelizer
     Netplex_log.logger_factories   (* allow all built-in logging styles *)