X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;fp=matitaB%2Fmatita%2Fmatitadaemon.ml;h=0c0f6cefda58da86b44c768b1d2d6c778d06004d;hb=e499c2e36d8a39c4749b8e0e34438b49532d15b8;hp=081ce316538b6563bf38b55650cf1b13e7f458f2;hpb=11a20b624a4b5ed18008678cf6cd46dd9a32634d;p=helm.git

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 081ce3165..0c0f6cefd 100644
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -6,6 +6,9 @@ exception Disamb_error of string
 
 module Stack = Continuationals.Stack
 
+(* disable for debug *)
+let prerr_endline _ = ()
+
 let rt_path () = Helm_registry.get "matita.rt_base_dir" 
 
 let libdir uid = (rt_path ()) ^ "/users/" ^ uid 
@@ -200,8 +203,8 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script
       Printf.sprintf "\005A href=\"%s\"\006%s\005/A\006"
         (NReference.string_of_reference r) (NCicPp.r2s status true r)
     in
-    if trace = [] then "{}"
-    else String.concat ", " 
+    (*if trace = [] then "{}"
+    else*) String.concat ", " 
       (HExtlib.filter_map (function 
         | NotationPt.NRef r -> Some (href r) 
         | _ -> None)
@@ -345,8 +348,7 @@ let load_doc filename outchan =
   Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan
 ;;
 
-let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
-  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+let retrieve (cgi : Netcgi.cgi_activation) =
   let env = cgi#environment in
   (try 
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
@@ -445,33 +447,54 @@ let advance0 sid text =
   let history = MatitaAuthentication.get_history sid in
   let status = status#reset_disambiguate_db () in
   let (st,new_statements,new_unparsed),parsed_len =
-    try
-      eval_statement !include_paths (*buffer*) status (`Raw text)
-    with
-    | HExtlib.Localized (floc,e) as exn ->
+    let rec do_exc = function
+    | HExtlib.Localized (floc,e) -> 
       let x, y = HExtlib.loc_of_floc floc in
-  prerr_endline (Printf.sprintf "ustring_sub caso 2: (%d,%d) parsed=%s" 0 x text);
       let pre = Netconversion.ustring_sub `Enc_utf8  0 x text in
-  prerr_endline (Printf.sprintf "ustring_sub caso 3: (%d,%d) parsed=%s" x (y-x) text);
       let err = Netconversion.ustring_sub `Enc_utf8  x (y-x) text in
-  prerr_endline (Printf.sprintf "ustring_sub caso 4: (%d,%d) parsed=%s" y (Netconversion.ustring_length `Enc_utf8 text - y) text);
       let post = Netconversion.ustring_sub `Enc_utf8 y 
          (Netconversion.ustring_length `Enc_utf8 text - y) text in
-      let _,title = MatitaExcPp.to_string exn in
+      let _,title = MatitaExcPp.to_string e in
       (* let title = "" in *)
       let marked = 
 	pre ^ "\005span class=\"error\" title=\"" ^ title ^ "\"\006" ^ err ^ "\005/span\006" ^ post in
       let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false 
       () (html_of_matita marked) in
-      raise (Emphasized_error marked) 
+      raise (Emphasized_error marked)
+    | Disambiguate.NoWellTypedInterpretation (floc,e) ->
+      let x, y = HExtlib.loc_of_floc floc in
+      let pre = Netconversion.ustring_sub `Enc_utf8  0 x text in
+      let err = Netconversion.ustring_sub `Enc_utf8  x (y-x) text in
+      let post = Netconversion.ustring_sub `Enc_utf8 y 
+         (Netconversion.ustring_length `Enc_utf8 text - y) text in
+      (*let _,title = MatitaExcPp.to_string e in*)
+      (* let title = "" in *)
+      let marked = 
+	pre ^ "\005span class=\"error\" title=\"" ^ e ^ "\"\006" ^ err ^ "\005/span\006" ^ post in
+      let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false 
+      () (html_of_matita marked) in
+      raise (Emphasized_error marked)
+    | NCicRefiner.Uncertain m as exn ->
+      let floc, e = Lazy.force m in
+      let x, y = HExtlib.loc_of_floc floc in
+      let pre = Netconversion.ustring_sub `Enc_utf8  0 x text in
+      let err = Netconversion.ustring_sub `Enc_utf8  x (y-x) text in
+      let post = Netconversion.ustring_sub `Enc_utf8 y 
+         (Netconversion.ustring_length `Enc_utf8 text - y) text in
+      (* let _,title = MatitaExcPp.to_string e in *)
+      (* let title = "" in *)
+      let marked = 
+	pre ^ "\005span class=\"error\" title=\"" ^ e ^ "\"\006" ^ err ^ "\005/span\006" ^ post in
+      let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false 
+      () (html_of_matita marked) in
+      raise (Emphasized_error marked)
     | NTacStatus.Error (s,None) as e ->
         prerr_endline 
-          ("NTacStatus.Error " ^ (Lazy.force s));
-        raise e
+          ("NTacStatus.Error " ^ (Lazy.force s)); raise e
     | NTacStatus.Error (s,Some exc) as e ->
         prerr_endline 
           ("NTacStatus.Error " ^ Lazy.force s ^ " -- " ^ (Printexc.to_string exc));
-        raise e
+        do_exc exc
     | GrafiteDisambiguate.Ambiguous_input (loc,choices) ->
       let x,y = HExtlib.loc_of_floc loc in
       let choice_of_alias = function
@@ -515,22 +538,32 @@ let advance0 sid text =
       in raise (Disamb_error strchoices)
    | GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l))
    (* | End_of_file -> ...          *)
+   | e -> raise e
+   in
+
+    try
+      eval_statement !include_paths (*buffer*) status (`Raw text)
+    with e -> do_exc e
   in
   MatitaAuthentication.set_status sid st;
   MatitaAuthentication.set_history sid (st::history);
+(*  prerr_endline "previous timestamp";
+  status#print_timestamp();
+  prerr_endline "current timestamp";
+  st#print_timestamp(); *)
   parsed_len, 
     Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false 
       () (html_of_matita new_statements), new_unparsed, st
 
-let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
-  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+let register (cgi : Netcgi.cgi_activation) =
   let _env = cgi#environment in
   
   assert (cgi#arguments <> []);
   let uid = cgi#argument_value "userid" in
   let userpw = cgi#argument_value "password" in
-  (try 
-    MatitaAuthentication.add_user uid userpw;
+  (try
+    (* currently registering only unprivileged users *) 
+    MatitaAuthentication.add_user uid userpw false;
 (*    env#set_output_header_field "Location" "/index.html" *)
     cgi#out_channel#output_string
      ("<html><head><meta http-equiv=\"refresh\" content=\"2;url=/login.html\">"
@@ -554,8 +587,7 @@ let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
-let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
-  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+let login (cgi : Netcgi.cgi_activation) =
   let env = cgi#environment in
   
   assert (cgi#arguments <> []);
@@ -563,6 +595,7 @@ let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let userpw = cgi#argument_value "password" in
   (try 
       MatitaAuthentication.check_pw uid userpw;
+      NCicLibrary.init (Some uid);
       let ft = MatitaAuthentication.read_ft uid in
       let _ = MatitaFilesystem.html_of_library uid ft in
        let sid = MatitaAuthentication.create_session uid in
@@ -584,8 +617,7 @@ let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
-let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
-  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+let logout (cgi : Netcgi.cgi_activation) =
   let env = cgi#environment in
   (try 
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
@@ -609,8 +641,7 @@ let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 
 exception File_already_exists;;
 
-let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
-  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+let save (cgi : Netcgi.cgi_activation) =
   let env = cgi#environment in
   (try 
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
@@ -676,10 +707,12 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
-let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
-  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
-  let _env = cgi#environment in
+let initiate_commit (cgi : Netcgi.cgi_activation) =
+  let env = cgi#environment in
   (try
+    let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
+    let sid = HExtlib.unopt sid in
+    MatitaAuthentication.probe_commit_priv sid;
     let out = do_global_commit () in
     cgi # set_header 
       ~cache:`No_cache 
@@ -699,13 +732,13 @@ let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
-let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
-  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+let svn_update (cgi : Netcgi.cgi_activation) =
   let env = cgi#environment in
   let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
   let sid = HExtlib.unopt sid in
   let uid = MatitaAuthentication.user_of_session sid in
   (try
+    MatitaAuthentication.probe_commit_priv sid;
     let files,anomalies,(added,conflict,del,upd,merged) = 
       MatitaFilesystem.update_user uid 
     in
@@ -743,8 +776,9 @@ let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 
 (* returns the length of the executed text and an html representation of the
  * current metasenv*)
-let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
-  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+(*let advance  =*)
+let advance (cgi : Netcgi.cgi_activation) =
+  (* let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in *)
   let env = cgi#environment in
   (try 
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
@@ -796,13 +830,11 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
-let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
-  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+let gotoBottom (cgi : Netcgi.cgi_activation) =
   let env = cgi#environment in
 (*  (try  *)
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
     let sid = HExtlib.unopt sid in
-    let history = MatitaAuthentication.get_history sid in
 
     let error_msg = function
       | Emphasized_error text -> "<localized>" ^ text ^ "</localized>" 
@@ -819,11 +851,12 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
         prerr_endline ("evaluating: " ^ first_line text);
         let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in
         aux ((plen,new_parsed)::acc) new_unparsed
-      with e -> 
+      with e -> acc, error_msg e 
+        (* DON'T SERIALIZE NOW!!!
           let status = MatitaAuthentication.get_status sid in
           GrafiteTypes.Serializer.serialize 
             ~baseuri:(NUri.uri_of_string status#baseuri) status;
-          acc, error_msg e
+          acc, error_msg e *)
     in
     (* 
     cgi # set_header 
@@ -857,8 +890,7 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work() 
 ;;
 
-let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
-  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+let gotoTop (cgi : Netcgi.cgi_activation) =
   let env = cgi#environment in
   prerr_endline "executing goto Top";
   (try 
@@ -894,8 +926,7 @@ let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work() 
 ;;
 
-let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
-  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+let retract (cgi : Netcgi.cgi_activation) =
   let env = cgi#environment in
   (try  
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
@@ -907,13 +938,18 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
       ();
     *)
     let history = MatitaAuthentication.get_history sid in
+    let old_status = MatitaAuthentication.get_status sid in
     let new_history,new_status =
        match history with
          _::(status::_ as history) ->
           history, status
       | [_] -> (prerr_endline "singleton";failwith "retract")
       | _ -> (prerr_endline "nil"; assert false) in
-    prerr_endline ("prima della time travel");
+(*    prerr_endline "timestamp prima della retract";
+    old_status#print_timestamp ();
+    prerr_endline "timestamp della retract";
+    new_status#print_timestamp ();
+    prerr_endline ("prima della time travel"); *)
     NCicLibrary.time_travel new_status;
     prerr_endline ("dopo della time travel");
     MatitaAuthentication.set_history sid new_history;
@@ -934,8 +970,7 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 ;;
 
 
-let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
-  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+let viewLib (cgi : Netcgi.cgi_activation) =
   let env = cgi#environment in
   
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
@@ -974,8 +1009,7 @@ let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   
 ;;
 
-let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
-  let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+let resetLib (cgi : Netcgi.cgi_activation) =
   MatitaAuthentication.reset ();
     cgi # set_header 
       ~cache:`No_cache