let str = Ulexing.from_utf8_channel stdin in
try
run_script str
- (MatitaEngine.eval_from_stream_greedy
+ (MatitaEngine.eval_from_stream ~prompt:true
~include_paths:(Helm_registry.get_list Helm_registry.string
"matita.includes"))
with
let go () =
Helm_registry.load_from BuildTimeConf.matita_conf;
- CicNotation.load_notation BuildTimeConf.core_notation_script;
+ CicNotation2.load_notation BuildTimeConf.core_notation_script;
Http_getter.init ();
MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
LibraryDb.create_owner_environment ();
CicEnvironment.set_trust (* environment trust *)
(let trust = Helm_registry.get_bool "matita.environment_trust" in
fun _ -> trust);
- status := Some (ref (Lazy.force MatitaEngine.initial_status));
+ status := Some (ref (MatitaSync.init ()));
Sys.catch_break true;
interactive_loop ()
MatitaInit.initialize_all ();
(* must be called after init since args are set by cmdline parsing *)
let fname = fname () in
- status := Some (ref (Lazy.force MatitaEngine.initial_status));
+ status := Some (ref (MatitaSync.init ()));
Sys.catch_break true;
let origcb = HLog.get_log_callback () in
let newcb tag s =
Ulexing.from_utf8_channel
(match fname with
| "stdin" -> stdin
- | fname -> open_in fname)
- in
- run_script is
- (MatitaEngine.eval_from_stream
- ~include_paths:(Helm_registry.get_list Helm_registry.string
- "matita.includes")
- ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve")));
+ | fname -> open_in fname) in
+ let include_paths =
+ Helm_registry.get_list Helm_registry.string "matita.includes" in
+ (try
+ run_script is
+ (MatitaEngine.eval_from_stream ~include_paths
+ ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve")))
+ with End_of_file -> ());
let elapsed = Unix.time () -. time in
let tm = Unix.gmtime elapsed in
let sec =
else
begin
let basedir = Helm_registry.get "matita.basedir" in
- let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in
- let metadata_fname = GrafiteMisc.metadata_file_of_script ~basedir fname in
+ let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths fname in
+ let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
+ let metadata_fname = LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
GrafiteMarshal.save_moo moo_fname moo_content_rev;
LibraryNoDb.save_metadata metadata_fname metadata;
HLog.message