- | MatitaEngine.Drop -> pp_ocaml_mode ()
- | Sys.Break -> MatitaLog.error "user break!"; go ()
- | MatitaTypes.Command_error _ -> go ()
- | CicTextualParser2.Parse_error (floc,err) ->
- (* check for EOI *)
- if Stream.peek str = None then
- exit 0
- else
- 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 ()
-
-let main ~mode =
- at_exit
- (fun () ->
- Http_getter_logger.log "Sync map tree to disk...";
- Http_getter.sync_dump_file ();
- print_endline "\nThanks for using Matita!\n");
+ | GrafiteEngine.Drop -> pp_ocaml_mode ()
+ | GrafiteEngine.Macro (floc,_) ->
+ let x, y = HExtlib.loc_of_floc floc in
+ HLog.error
+ (sprintf "A macro has been found in a script at %d-%d" x y);
+ interactive_loop ()
+ | Sys.Break -> HLog.error "user break!"; interactive_loop ()
+ | GrafiteTypes.Command_error _ -> interactive_loop ()
+ | End_of_file ->
+ print_newline ();
+ clean_exit (Some 0)
+ | HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
+ let x, y = HExtlib.loc_of_floc floc in
+ HLog.error (sprintf "Parse error at %d-%d: %s" x y err);
+ interactive_loop ()
+ | exn -> HLog.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");
+ LibraryDb.create_owner_environment ();
+ CicEnvironment.set_trust (* environment trust *)
+ (let trust = Helm_registry.get_bool "matita.environment_trust" in
+ fun _ -> trust);
+ let include_paths =
+ Helm_registry.get_list Helm_registry.string "matita.includes" in
+ grafite_status := Some (GrafiteSync.init ());
+ lexicon_status :=
+ Some (CicNotation2.load_notation ~include_paths
+ BuildTimeConf.core_notation_script);