From 441cd9b8db014ea11f5afc46f192a3d73eee6a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 9 Dec 2008 08:57:39 +0000 Subject: [PATCH] option to collapse all tex macros implemented --- helm/software/matita/matita.ml | 5 ++- helm/software/matita/matitaScript.ml | 62 ++++++++++++++------------- helm/software/matita/matitaScript.mli | 1 + 3 files changed, 37 insertions(+), 31 deletions(-) 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 -- 2.39.2