the decentralization of core notation continues ...

[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 184a6937cf3cc336348fede07f61041ef59b4178..ccf2ffa6a6cdcdb7bfb022297993b3ea4dc5bf27 100644 (file)
--- a/matita/components/binaries/matex/TeX.ml
+++ b/matita/components/binaries/matex/TeX.ml
@@ -17,6 +17,7 @@ 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 *)
 
@@ -31,8 +32,8 @@ 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 mk_rev_args riss is =
+   X.rev_map_append group ([] :: riss) is
 
 let rev_mk_args iss is =
    free "" :: X.rev_map_append group iss is