open Printf
-open MatitaTypes
+open GrafiteTypes
(** {2 Initialization} *)
try
eval_function status is cb
with
- | MatitaEngine.Drop
+ | GrafiteEngine.Drop
| End_of_file
| CicNotationParser.Parse_error _ as exn -> raise exn
| exn ->
None -> opt_exit n
| Some status ->
try
- let baseuri = MatitaTypes.get_string_option !status "baseuri" in
+ let baseuri = GrafiteTypes.get_string_option !status "baseuri" in
let basedir = Helm_registry.get "matita.basedir" in
LibraryClean.clean_baseuris ~basedir ~verbose:false [baseuri];
opt_exit n
- with MatitaTypes.Option_error("baseuri", "not found") ->
+ with GrafiteTypes.Option_error("baseuri", "not found") ->
(* no baseuri ==> nothing to clean yet *)
opt_exit n
~include_paths:(Helm_registry.get_list Helm_registry.string
"matita.includes"))
with
- | MatitaEngine.Drop -> pp_ocaml_mode ()
+ | GrafiteEngine.Drop -> pp_ocaml_mode ()
| Sys.Break -> HLog.error "user break!"; interactive_loop ()
- | MatitaTypes.Command_error _ -> interactive_loop ()
+ | GrafiteTypes.Command_error _ -> interactive_loop ()
| End_of_file ->
print_newline ();
clean_exit (Some 0)
| Some s -> !s.proof_status, !s.moo_content_rev, !s
| None -> assert false
in
- if proof_status <> MatitaTypes.No_proof then
+ if proof_status <> GrafiteTypes.No_proof then
begin
HLog.error
"there are still incomplete proofs at the end of the script";
else
begin
let basedir = Helm_registry.get "matita.basedir" in
- let moo_fname = MatitaMisc.obj_file_of_script ~basedir fname in
+ let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in
GrafiteMarshal.save_moo moo_fname moo_content_rev;
HLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
clean_exit (Some ~-1)
else
pp_ocaml_mode ()
- | MatitaEngine.Drop ->
+ | GrafiteEngine.Drop ->
if mode = `COMPILER then
clean_exit (Some 1)
else