X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=1e5a0c70037b8308d27ae73fa3a10005601ffdba;hb=100184e7920cc3c70b50b694a17fa40ecde45e77;hp=081ce316538b6563bf38b55650cf1b13e7f458f2;hpb=0d0fca7f894b1aadd4840d550b65183fc4a9c124;p=helm.git

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 081ce3165..1e5a0c700 100644
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -6,6 +6,10 @@ exception Disamb_error of string
 
 module Stack = Continuationals.Stack
 
+let debug = prerr_endline
+(* 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 +204,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)
@@ -445,33 +449,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 +540,40 @@ let advance0 sid text =
       in raise (Disamb_error strchoices)
    | GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l))
    (* | End_of_file -> ...          *)
+   | e -> 
+      prerr_endline ("matitadaemon *** Unhandled exception " ^ Printexc.to_string e);
+      raise e
+   in
+
+    try
+      eval_statement !include_paths (*buffer*) status (`Raw text)
+    with e -> do_exc e
   in
+        debug "BEGIN PRINTGRAMMAR";
+        (*prerr_endline (Print_grammar.ebnf_of_term status);*)
+        (*let kwds = String.concat ", " status#get_kwds in
+        debug ("keywords = " ^ kwds );*)
+        debug "END PRINTGRAMMAR";
   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 register  (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   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,7 +597,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 login  (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   let env = cgi#environment in
   
@@ -563,6 +606,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,7 +628,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 logout  (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   let env = cgi#environment in
   (try 
@@ -609,7 +653,7 @@ let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 
 exception File_already_exists;;
 
-let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+let save  (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   let env = cgi#environment in
   (try 
@@ -678,8 +722,11 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 
 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 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 +746,14 @@ 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 svn_update  (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   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,6 +791,7 @@ 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  =*)
 let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   let env = cgi#environment in
@@ -796,13 +845,12 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
-let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+let gotoBottom  (cgi : Netcgi1_compat.Netcgi_types.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
     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 +867,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,7 +906,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 gotoTop  (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   let env = cgi#environment in
   prerr_endline "executing goto Top";
@@ -894,7 +943,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 retract  (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
   let env = cgi#environment in
   (try  
@@ -907,13 +956,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,7 +988,7 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
 ;;
 
 
-let viewLib (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 env = cgi#environment in
   
@@ -974,7 +1028,7 @@ let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
   
 ;;
 
-let resetLib (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
   MatitaAuthentication.reset ();
     cgi # set_header