- scope management begins...

[helm.git] / matita / components / binaries / matex / TeX.ml

diff --git a/matita/components/binaries/matex/TeX.ml b/matita/components/binaries/matex/TeX.ml
index c213d4d9629a689379f39cb0068e13bd4d2fbbfe..184a6937cf3cc336348fede07f61041ef59b4178 100644 (file)
--- a/matita/components/binaries/matex/TeX.ml
+++ b/matita/components/binaries/matex/TeX.ml
@@ -11,7 +11,10 @@
 
 module L = List
 
+module X = Ground
+
 type item = Free  of string  (* free text *)
+          | Text  of string  (* quoted text *)
           | Macro of string  (* macro *)
           | Group of text    (* group *)
          
@@ -19,16 +22,17 @@ and text = item list         (* structured text *)
 
 let file_ext = ".tex"
 
-let empty = [Free ""]
-
-let newline = [Free "%\n"]
-
 let group s = Group s
 
-let arg s = Group [Free s]
+let arg s = Group [Text s]
 
-let mk_rev_args riss =
-   L.rev_map group (empty :: riss)
+let free s = Group [Free s]
 
 let mk_segs us =
    L.rev_map arg ("" :: (L.rev us))
+
+let mk_rev_args riss =
+   L.rev_map group ([] :: riss)
+
+let rev_mk_args iss is =
+   free "" :: X.rev_map_append group iss is