Procedural: we removed some commented code

[helm.git] / helm / software / matita / matitacLib.ml

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index b33590a0ae95127a7afb7ae0dff0576342626cb0..9c331d2ee2da2bf2a0bc9d692aa9c58543c4f451 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -259,11 +259,13 @@ let compile options fname =
      with MatitaEngine.EnrichedWithLexiconStatus 
             (GrafiteEngine.Macro (floc, f), lex_status) as exn ->
             match f (get_macro_context (Some grafite_status)) with 
-            | _, GrafiteAst.Inline (_, style, suri, prefix) ->
+            | _, GrafiteAst.Inline (_, style, suri, prefix, flavour) ->
               let str =
-               ApplyTransformation.txt_of_inline_macro style suri prefix
-                ~map_unicode_to_tex:(Helm_registry.get_bool
-                  "matita.paste_unicode_as_tex") in
+               ApplyTransformation.txt_of_inline_macro style prefix suri
+                ?flavour
+               ~map_unicode_to_tex:(Helm_registry.get_bool
+                  "matita.paste_unicode_as_tex")
+             in
               !out str;
               aux_for_dump x
             |_-> raise exn
@@ -371,7 +373,11 @@ module F =
           let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in
          let atexit = dump generated in
          let res = compile options fname in
-         atexit res
+         let r = atexit res in
+         if r then r else begin
+            Sys.remove generated;
+            Printf.printf "rm %s\n" generated; flush stdout; r
+         end
        else
           compile options fname