- let (x, y) = CicAst.loc_of_floc floc in
- MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
- go ()
- | exn -> MatitaLog.error (Printexc.to_string exn); go ()
+ (* check for EOI *)
+ if Stream.peek str = None then
+ begin
+ print_newline ();
+ clean_exit (Some 0)
+ end
+ else
+ let (x, y) = CicAst.loc_of_floc floc in
+ MatitaLog.error (sprintf "Parse error at %d-%d: %s" x y err);
+ interactive_loop ()
+ | exn -> MatitaLog.error (Printexc.to_string exn); interactive_loop ()
+
+let go () =
+ Helm_registry.load_from BuildTimeConf.matita_conf;
+ Http_getter.init ();
+ MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+ status := Some (ref (Lazy.force MatitaEngine.initial_status));
+ Sys.catch_break true;
+ interactive_loop ()
+
+let dump_moo_to_file file moo =
+ let os = open_out (MatitaMisc.obj_file_of_script file) in
+ let output s = output_string os s in
+ output "(* GENERATED FILE: DO NOT EDIT! *)\n\n";
+ List.iter output (List.rev moo);
+ close_out os