Huge commit with several changes:

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index a5e24d3150853ce71cf11e5662c31b480ecf0f30..b221919d2e33a38433f3216bcb3498718541c06a 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -346,8 +346,8 @@ let cic2grafite context menv t =
     let width = max_int in
     let term_pp content_term =
       let pres_term = TermContentPres.pp_ast content_term in
-      let dummy_tbl = Hashtbl.create 1 in
-      let markup = CicNotationPres.render dummy_tbl pres_term in
+      let lookup_uri = fun _ -> None in
+      let markup = CicNotationPres.render ~lookup_uri pres_term in
       let s = "(" ^ BoxPp.render_to_string
        ~map_unicode_to_tex:(Helm_registry.get_bool
          "matita.paste_unicode_as_tex")
@@ -512,7 +512,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
         let (_,menv,subst,_,_,_), _ = 
           ProofEngineTypes.apply_tactic
             (Auto.auto_tac ~dbd ~params
-              ~universe:grafite_status.GrafiteTypes.universe) proof_status
+              ~automation_cache:grafite_status.GrafiteTypes.automation_cache) 
+            proof_status
         in
         let proof_term = 
           let irl = 
@@ -548,7 +549,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
                   "matita.paste_unicode_as_tex")
                 ~skip_thm_and_qed:true
                 ~skip_initial_lambdas:how_many_lambdas
-                80 GrafiteAst.Declarative "" obj
+                80 [] obj
           else
             if true then
               (* use cic2grafite *)
@@ -559,7 +560,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
                 Helm_registry.get_bool "matita.paste_unicode_as_tex"
              in
              ApplyTransformation.procedural_txt_of_cic_term
-                 ~map_unicode_to_tex 78 cc proof_term
+                 ~map_unicode_to_tex 78 [] cc proof_term
         in
         let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in
         [],text,parsed_text_length
@@ -567,12 +568,12 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
         ProofEngineTypes.Fail _ as exn -> 
           raise exn
           (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *))
-  | TA.Inline (_,style,suri,prefix,flavour) ->
-       let str = 
+  | TA.Inline (_, suri, params) ->
+       let str = "\n\n" ^ 
          ApplyTransformation.txt_of_inline_macro
           ~map_unicode_to_tex:(Helm_registry.get_bool
             "matita.paste_unicode_as_tex")
-          style ?flavour prefix suri 
+          params suri 
        in
        [], str, String.length parsed_text
                                 
@@ -675,7 +676,7 @@ let initial_statuses baseuri =
    CicNotation2.load_notation ~include_paths:[]
      BuildTimeConf.core_notation_script 
  in
- let grafite_status = GrafiteSync.init baseuri in
+ let grafite_status = GrafiteSync.init lexicon_status baseuri in
   grafite_status,lexicon_status
 in
 let read_include_paths file =
@@ -848,9 +849,43 @@ object (self)
     | exc -> self#notify; raise exc
 
   method private getFuture =
-    buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark))
-      ~stop:buffer#end_iter ()
+    let lock = buffer#get_iter_at_mark (`MARK locked_mark) in
+    let text = buffer#get_text ~start:lock ~stop:buffer#end_iter () in
+    text
 
+  method expandAllVirtuals =
+    let lock = buffer#get_iter_at_mark (`MARK locked_mark) in
+    let text = buffer#get_text ~start:lock ~stop:buffer#end_iter () in
+    buffer#delete ~start:lock ~stop:buffer#end_iter;
+    let text = Pcre.replace ~pat:":=" ~templ:"\\def" text in
+    let text = Pcre.replace ~pat:"->" ~templ:"\\to" text in
+    let text = Pcre.replace ~pat:"=>" ~templ:"\\Rightarrow" text in
+    let text = 
+      Pcre.substitute_substrings 
+        ~subst:(fun str -> 
+           let pristine = Pcre.get_substring str 0 in
+           let input = 
+             if pristine.[0] = ' ' then
+               String.sub pristine 1 (String.length pristine -1) 
+             else pristine 
+           in
+           let input = 
+             if input.[String.length input-1] = ' ' then
+               String.sub input 0 (String.length input -1) 
+             else input
+           in
+           let before, after =  
+             if input = "\\forall" || 
+                input = "\\lambda" || 
+                input = "\\exists" then "","" else " ", " " 
+           in
+           try 
+             before ^ Glib.Utf8.from_unichar 
+               (snd (Virtuals.symbol_of_virtual input)) ^ after
+           with Virtuals.Not_a_virtual -> pristine) 
+        ~pat:" ?\\\\[a-zA-Z]+ ?" text
+    in
+    buffer#insert ~iter:lock text
       
   (** @param rel_offset relative offset from current position of locked_mark *)
   method private moveMark rel_offset =