X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitacLib.ml;h=d82d3f7555db5a5c8335d62b290b0fc93c36137c;hb=3ea21b6d721c759876aa53385b421cb1412e11f5;hp=d57d211e21edde02b8c20beae7c5468f068e9bbb;hpb=2c4b1dbd4de1ae46da243b1adb9df2654bd0fb51;p=helm.git diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index d57d211e2..d82d3f755 100644 --- a/helm/matita/matitacLib.ml +++ b/helm/matita/matitacLib.ml @@ -36,16 +36,14 @@ let usage = sprintf "MatitaC v%s\nUsage: matitac [option ...] file\nOptions:" BuildTimeConf.version -let _ = - Helm_registry.load_from "matita.conf.xml"; - Http_getter.init (); - MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); - MatitaDb.clean_owner_environment (); - MatitaDb.create_owner_environment () - -let status = ref (Lazy.force MatitaEngine.initial_status) ;; +let status = ref None let run_script is eval_function = + let status = + match !status with + | None -> assert false + | Some s -> s + in let slash_n_RE = Pcre.regexp "\\n" in let cb status stm = (* dump_status status; *) @@ -102,6 +100,14 @@ let rec go () = | exn -> MatitaLog.error (Printexc.to_string exn); go () let main ~mode = + Helm_registry.load_from "matita.conf.xml"; + Http_getter.init (); + MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner"); +(* + MatitaDb.clean_owner_environment (); + MatitaDb.create_owner_environment (); +*) + status := Some (ref (Lazy.force MatitaEngine.initial_status)); at_exit (fun () -> Http_getter_logger.log "Sync map tree to disk..."; @@ -130,7 +136,11 @@ let main ~mode = let hou = if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else "" in - let proof_status = !status.proof_status in + let proof_status = + match !status with + | Some s -> !s.proof_status + | None -> assert false + in if proof_status <> MatitaTypes.No_proof then begin MatitaLog.error @@ -141,10 +151,16 @@ let main ~mode = begin MatitaLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); + close_out (open_out (MatitaMisc.obj_file_of_script fname)); exit 0 end with - | Sys.Break -> MatitaLog.error "user break!"; exit ~-1 + | Sys.Break -> + MatitaLog.error "user break!"; + if mode = `COMPILER then + exit ~-1 + else + pp_ocaml_mode () | MatitaEngine.Drop -> if mode = `COMPILER then exit 1 @@ -157,4 +173,4 @@ let main ~mode = if mode = `COMPILER then exit 1 else - go () + pp_ocaml_mode ()