]> matita.cs.unibo.it Git - helm.git/blobdiff - matitaB/matita/matitadaemon.ml
Multi-user matita: changed the status object to include a ``user'' method
[helm.git] / matitaB / matita / matitadaemon.ml
index ea63e1a084ba6d231695f693559e650a11b06d82..8dbfa45112cc9be7074e37969fe5bdd7f4d83dc8 100644 (file)
@@ -47,8 +47,8 @@ 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;;
 
@@ -203,6 +203,7 @@ let advance0 text =
      in
   status := st;
   history := st :: !history;
+  prerr_endline ("after advance0 history.length = " ^ string_of_int (List.length !history));
   parsed_len, new_unparsed
 
 
@@ -266,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() 
@@ -347,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 *)