From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 9 Dec 2008 08:57:39 +0000 (+0000)
Subject: option to collapse all tex macros implemented
X-Git-Tag: make_still_working~4431
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=441cd9b8db014ea11f5afc46f192a3d73eee6a39;p=helm.git

option to collapse all tex macros implemented
---

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index f8cc4efb4..9fa70e11f 100644
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -280,8 +280,9 @@ let _ =
         ~doc:(HExtlib.unopt (mview ())#get_document) ~name:"matita.xml" ())); *)
     addDebugItem "load (sequent) MathML from matita.xml"
       (fun _ -> (mview ())#load_uri ~filename:"matita.xml");
-    addDebugItem "autoWin"
-    (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status);
+    addDebugSeparator ();
+    addDebugItem "Expand virtuals"
+    (fun _ -> (MatitaScript.current ())#expandAllVirtuals);
   end
   (** Debugging }}} *)
 
diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 7bcbea294..7768e2287 100644
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -851,36 +851,40 @@ object (self)
     let lock = buffer#get_iter_at_mark (`MARK locked_mark) in
     let text = buffer#get_text ~start:lock ~stop:buffer#end_iter () in
     text
-(* THIS SNIPPET AUTOMATICALLY EXPANDS EVERY \TeX MACRO
-    if Pcre.pmatch ~pat:"\\\\[a-zA-Z]+" text then
-      begin
-        buffer#delete ~start:lock ~stop:buffer#end_iter;
-        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
-               try 
-                 Glib.Utf8.from_unichar (snd (Virtuals.symbol_of_virtual input))
-               with Virtuals.Not_a_virtual -> pristine) 
-            ~pat:" ?\\\\[a-zA-Z]+ ?" text
-        in
-        buffer#insert ~iter:lock text;
-        text
-      end
-    else
-      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 =
diff --git a/helm/software/matita/matitaScript.mli b/helm/software/matita/matitaScript.mli
index 3d9e8fba7..304818f7b 100644
--- a/helm/software/matita/matitaScript.mli
+++ b/helm/software/matita/matitaScript.mli
@@ -85,6 +85,7 @@ object
   
   (* debug *)
   method dump : unit -> unit
+  method expandAllVirtuals : unit 
 
 end