X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;fp=matitaB%2Fmatita%2Fmatitadaemon.ml;h=fd7696173b0d38ad589819802480729b82e7a5dc;hb=5310bb693a61b4c2c51bbd05e5ef9a4b764012cd;hp=1e5a0c70037b8308d27ae73fa3a10005601ffdba;hpb=0c442e9d5804a828b4a7ae6eb8a172ded6f477c9;p=helm.git

diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml
index 1e5a0c700..fd7696173 100644
--- a/matitaB/matita/matitadaemon.ml
+++ b/matitaB/matita/matitadaemon.ml
@@ -213,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
@@ -362,6 +382,7 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.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 = 
@@ -386,10 +407,11 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.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 = (MatitaAuthentication.get_status sid)#set_baseuri 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\""