+ pp_times fname false big_bang;
+ LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status;
+ clean_exit baseuri false
+ | MatitaEngine.EnrichedWithLexiconStatus (exn, lex_stat) ->
+ (match exn with
+ | Sys.Break -> HLog.error "user break!"
+ | GrafiteEngine.Macro (floc, f) ->
+ (try
+ match f (get_macro_context (Some grafite_status)) with
+ | _, GrafiteAst.Inline (_, style, suri, prefix) ->
+ let str =
+ ApplyTransformation.txt_of_inline_macro style suri prefix
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex") in
+ (* the output of compilation is wrong in this way!! *)
+ !out str; ignore(compile options fname)
+ | _ ->
+ let x, y = HExtlib.loc_of_floc floc in
+ HLog.error (sprintf "A macro has been found at %d-%d" x y)
+ with exn -> HLog.error (snd (MatitaExcPp.to_string exn)))
+ | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
+ let (x, y) = HExtlib.loc_of_floc floc in
+ HLog.error (sprintf "Parse error at %d-%d: %s" x y err)
+ | exn -> HLog.error (snd (MatitaExcPp.to_string exn)));
+ LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status;