X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitacLib.ml;h=9c331d2ee2da2bf2a0bc9d692aa9c58543c4f451;hb=ea3b15fdedb39c72ae1b39f210917c6f38fc062d;hp=b33590a0ae95127a7afb7ae0dff0576342626cb0;hpb=662f191b09d1b9e3d13e4f9ee5c174c1ac08fadb;p=helm.git

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index b33590a0a..9c331d2ee 100644
--- 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