| End_of_file
| CicNotationParser.Parse_error _ as exn -> raise exn
| exn ->
- MatitaLog.error (MatitaExcPp.to_string exn);
+ MatitaLog.error (snd (MatitaExcPp.to_string exn));
raise exn
let fname () =
| End_of_file ->
print_newline ();
clean_exit (Some 0)
- | CicNotationParser.Parse_error (floc,err) ->
- let (x, y) = CicNotationPt.loc_of_floc floc in
+ | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
+ let (x, y) = HExtlib.loc_of_floc floc in
MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
interactive_loop ()
| exn -> MatitaLog.error (Printexc.to_string exn); interactive_loop ()
in
if Helm_registry.get_bool "matita.quiet" then
MatitaLog.set_log_callback newcb;
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
try
let time = Unix.time () in
if Helm_registry.get_bool "matita.quiet" then
end
else
begin
- let moo_fname = MatitaMisc.obj_file_of_script fname in
+ let moo_fname = MatitacleanLib.obj_file_of_script fname in
MatitaMoo.save_moo moo_fname moo_content_rev;
MatitaLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
clean_exit (Some 1)
else
pp_ocaml_mode ()
- | CicNotationParser.Parse_error (floc,err) ->
- let (x, y) = CicNotationPt.loc_of_floc floc in
+ | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
+ let (x, y) = HExtlib.loc_of_floc floc in
MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
if mode = `COMPILER then
clean_exit (Some 1)
else
pp_ocaml_mode ()
| exn ->
- if Helm_registry.get_bool "matita.debug" then raise exn;
+ if matita_debug then raise exn;
if mode = `COMPILER then
clean_exit (Some 3)
else