X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2FTeX.ml;h=ccf2ffa6a6cdcdb7bfb022297993b3ea4dc5bf27;hb=59fd7b5ea24e71b47aee069440f140bcccf1292a;hp=d5eb305dbd5cd61038321323290b9066d8edb470;hpb=2ffd7e47f1872878f6af4084074655da5cf3b23e;p=helm.git

diff --git a/matita/components/binaries/matex/TeX.ml b/matita/components/binaries/matex/TeX.ml
index d5eb305db..ccf2ffa6a 100644
--- a/matita/components/binaries/matex/TeX.ml
+++ b/matita/components/binaries/matex/TeX.ml
@@ -11,20 +11,29 @@
 
 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 *)
+          | Note  of string  (* comment *)
          
 and text = item list         (* structured text *)
 
 let file_ext = ".tex"
 
-let empty = [Free ""]
+let group s = Group s
+
+let arg s = Group [Text s]
+
+let free s = Group [Free s]
 
-let newline = [Free "%\n"]
+let mk_segs us =
+   L.rev_map arg ("" :: (L.rev us))
 
-let arg s = Group [Free s]
+let mk_rev_args riss is =
+   X.rev_map_append group ([] :: riss) is
 
-let mk_rev_args riss =
-   L.rev_map (fun t -> Group t) (empty :: riss)
- 
+let rev_mk_args iss is =
+   free "" :: X.rev_map_append group iss is