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
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