- transcript: bugfix

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

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index d8e66dbf2040c5c27530e02af3078945657c603c..3ff2d034901f15bbf175e2630dc993d90d3356f8 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -76,7 +76,6 @@ let eval_with_engine include_paths guistuff lexicon_status grafite_status user_g
 =
   let module TAPp = GrafiteAstPp in
   let module DTE = DisambiguateTypes.Environment in
-  let module DP = DisambiguatePp in
   let parsed_text_length =
     String.length skipped_txt + String.length nonskipped_txt 
   in
@@ -94,8 +93,8 @@ let eval_with_engine include_paths guistuff lexicon_status grafite_status user_g
       (fun (acc, to_prepend) (status,alias) ->
        match alias with
        | None -> (status,to_prepend ^ nonskipped_txt)::acc,""
-       | Some (k,((v,_) as value)) ->
-            let newtxt = DP.pp_environment (DTE.add k value DTE.empty) in
+       | Some (k,value) ->
+            let newtxt = LexiconAstPp.pp_alias value in
             (status,to_prepend ^ newtxt ^ "\n")::acc, "")
       ([],skipped_txt) enriched_history_fragment
   in
@@ -676,7 +675,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 =
@@ -849,9 +848,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 =