Matitaweb: opening a file resets the status.

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

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 0c0f6cefda58da86b44c768b1d2d6c778d06004d..261811815d3c1705d41de529c789ac19cb9ad4a9 100644 (file)
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -6,6 +6,7 @@ exception Disamb_error of string
 
 module Stack = Continuationals.Stack
 
+let debug = prerr_endline
 (* disable for debug *)
 let prerr_endline _ = ()
 
@@ -212,6 +213,26 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script
   in
   
   match ast with
+  | GrafiteAst.Executable (_,
+      GrafiteAst.NCommand (_,
+        GrafiteAst.NObj (loc, astobj,_))) ->
+          let objname = NotationPt.name_of_obj astobj in
+          let status = 
+            MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast)
+          in
+          let new_parsed_text = Ulexing.from_utf8_string parsed_text in
+          let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in
+          let outstr = ref "" in
+          ignore (SmallLexer.mk_small_printer interpr outstr new_parsed_text);
+          let x, y = HExtlib.loc_of_floc floc in
+          let pre = Netconversion.ustring_sub `Enc_utf8  0 x !outstr in
+          let post = Netconversion.ustring_sub `Enc_utf8 x
+           (Netconversion.ustring_length `Enc_utf8 !outstr - x) !outstr in
+          outstr := Printf.sprintf 
+            "%s\005input type=\"radio\" class=\"anchor\" id=\"%s\" /\006%s" pre objname post;
+          prerr_endline ("baseuri after advance = " ^ status#baseuri);
+          (* prerr_endline ("parser output: " ^ !outstr); *)
+          (status,!outstr, unparsed_txt'),parsed_text_len
   | GrafiteAst.Executable (_,
       GrafiteAst.NTactic (_,
         [GrafiteAst.NAuto (_, (l,a as auto_params))])) when is_auto auto_params
@@ -348,7 +369,8 @@ let load_doc filename outchan =
   Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan
 ;;
 
-let retrieve (cgi : Netcgi.cgi_activation) =
+let retrieve (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
@@ -360,6 +382,7 @@ let retrieve (cgi : Netcgi.cgi_activation) =
       ~content_type:"text/xml; charset=\"utf-8\""
       ();
     *)
+    let readonly = cgi # argument_value "readonly" in
     let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in
     (* prerr_endline ("reading file " ^ filename); *)
     let body = 
@@ -384,16 +407,23 @@ let retrieve (cgi : Netcgi.cgi_activation) =
        with 
          Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in
     include_paths := incpaths;
-    let status = (MatitaAuthentication.get_status sid)#set_baseuri baseuri in
-    let history = [status] in
-    MatitaAuthentication.set_status sid status;
-    MatitaAuthentication.set_history sid history;
+    if readonly <> "true" then
+       (let status = new MatitaEngine.status (Some uid) baseuri in
+        let history = [status] in
+        MatitaAuthentication.set_status sid status;
+        MatitaAuthentication.set_history sid history);
     cgi # set_header 
       ~cache:`No_cache 
       ~content_type:"text/xml; charset=\"utf-8\""
       ();
     cgi#out_channel#output_string body;
   with
+  | Sys_error _ -> 
+    cgi # set_header 
+      ~cache:`No_cache 
+      ~content_type:"text/xml; charset=\"utf-8\""
+      ();
+    cgi#out_channel#output_string "<error />"
   | Not_found _ -> 
     cgi # set_header
       ~status:`Internal_server_error
@@ -538,13 +568,20 @@ 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
+   | 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";
@@ -555,7 +592,8 @@ let advance0 sid text =
     Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false 
       () (html_of_matita new_statements), new_unparsed, st
 
-let register (cgi : Netcgi.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 <> []);
@@ -587,7 +625,8 @@ let register (cgi : Netcgi.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
-let login (cgi : Netcgi.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
   
   assert (cgi#arguments <> []);
@@ -617,7 +656,8 @@ let login (cgi : Netcgi.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
-let logout (cgi : Netcgi.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 
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
@@ -641,7 +681,8 @@ let logout (cgi : Netcgi.cgi_activation) =
 
 exception File_already_exists;;
 
-let save (cgi : Netcgi.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 
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
@@ -707,7 +748,8 @@ let save (cgi : Netcgi.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
-let initiate_commit (cgi : Netcgi.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
   (try
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
@@ -732,7 +774,8 @@ let initiate_commit (cgi : Netcgi.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
-let svn_update (cgi : Netcgi.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
@@ -777,8 +820,8 @@ let svn_update (cgi : Netcgi.cgi_activation) =
 (* returns the length of the executed text and an html representation of the
  * current metasenv*)
 (*let advance  =*)
-let advance (cgi : Netcgi.cgi_activation) =
-  (* let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in *)
+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
   (try 
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
@@ -830,7 +873,8 @@ let advance (cgi : Netcgi.cgi_activation) =
   cgi#out_channel#commit_work()
 ;;
 
-let gotoBottom (cgi : Netcgi.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
@@ -890,7 +934,8 @@ let gotoBottom (cgi : Netcgi.cgi_activation) =
   cgi#out_channel#commit_work() 
 ;;
 
-let gotoTop (cgi : Netcgi.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";
   (try 
@@ -926,7 +971,8 @@ let gotoTop (cgi : Netcgi.cgi_activation) =
   cgi#out_channel#commit_work() 
 ;;
 
-let retract (cgi : Netcgi.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  
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
@@ -970,7 +1016,8 @@ let retract (cgi : Netcgi.cgi_activation) =
 ;;
 
 
-let viewLib (cgi : Netcgi.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
   
     let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
@@ -1009,7 +1056,8 @@ let viewLib (cgi : Netcgi.cgi_activation) =
   
 ;;
 
-let resetLib (cgi : Netcgi.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 
       ~cache:`No_cache