+ let status = ref (Lazy.force MatitaEngine.initial_status) in
+ try
+ while true do
+ dump_status !status;
+ try
+ status := MatitaEngine.eval_from_stream !status is
+ with
+ | CicTextualParser2.Parse_error _ as exn ->
+ try
+ Stream.empty is;
+ raise End_of_file
+ with Stream.Failure -> raise exn
+ | exn ->
+ MatitaLog.error (Printexc.to_string exn);
+ raise exn
+ done
+ with
+ | End_of_file ->
+ MatitaLog.message (sprintf "execution of %s completed." fname);
+ Http_getter.sync_dump_file ();
+ exit(0)
+ | CicTextualParser2.Parse_error (floc,err) ->
+ let (x, y) = CicAst.loc_of_floc floc in
+ MatitaLog.message (sprintf "Parse error at %d-%d: %s" x y err);
+ Http_getter.sync_dump_file ();
+ exit 1
+