exception AttemptToInsertAnAlias
+let out = ref ignore
+
+let set_callback f = out := f
+
let pp_ast_statement =
GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
- ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:CicNotationPp.pp_obj
+ ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term)
(** {2 Initialization} *)
in
HLog.debug ("Executing: ``" ^ stm ^ "''"))
in
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
try
- let grafite_status'', lexicon_status'' =
- match eval_function lexicon_status' grafite_status' is cb with
- [] -> assert false
- | (s,None)::_ -> s
- | (s,Some _)::_ -> raise AttemptToInsertAnAlias
- in
- lexicon_status := Some lexicon_status'';
- grafite_status := Some grafite_status''
+ match eval_function lexicon_status' grafite_status' is cb with
+ [] -> raise End_of_file
+ | ((grafite_status'',lexicon_status''),None)::_ ->
+ lexicon_status := Some lexicon_status'';
+ grafite_status := Some grafite_status''
+ | (s,Some _)::_ -> raise AttemptToInsertAnAlias
with
| GrafiteEngine.Drop
| End_of_file
| CicNotationParser.Parse_error _ as exn -> raise exn
| exn ->
- HLog.error (snd (MatitaExcPp.to_string exn));
+ if not matita_debug then
+ HLog.error (snd (MatitaExcPp.to_string exn)) ;
raise exn
let fname () =
"matita.includes"))
with
| GrafiteEngine.Drop -> pp_ocaml_mode ()
- | GrafiteEngine.Macro (floc,_) ->
- let x, y = HExtlib.loc_of_floc floc in
+ | GrafiteEngine.Macro (floc, f) ->
+ begin match snd (f []) with
+ | GrafiteAst.Inline (_, style, suri, prefix) ->
+ let str = ApplyTransformation.txt_of_inline_macro style suri prefix in
+ !out str
+ | _ -> ()
+ end;
+ let x, y = HExtlib.loc_of_floc floc in
HLog.error
(sprintf "A macro has been found in a script at %d-%d" x y);
interactive_loop ()
else
"matitac"
in
- let rc = if rc then "OK" else "FAIL" in
+ let rc = if rc then "\e[0;32mOK\e[0m" else "\e[0;31mFAIL\e[0m" in
let times =
let fmt t =
let seconds = int_of_float t in
end
else
begin
- let baseuri =
+ let baseuri, _fullpathforfname =
DependenciesParser.baseuri_of_script ~include_paths fname in
let moo_fname =
LibraryMisc.obj_file_of_baseuri
exit 0
end
with
- | Sys.Break ->
+ | Sys.Break as exn ->
+ if matita_debug then raise exn;
HLog.error "user break!";
pp_times fname bench_mode false big_bang;
if mode = `COMPILER then