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
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 =
| "stdin" -> stdin
| fname -> open_in fname) in
let include_paths =
- Helm_registry.get_list Helm_registry.string "matita.includes"
- in
- run_script is
- (MatitaEngine.eval_from_stream ~include_paths
- ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve")));
+ 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 =