~user:(Helm_registry.get "db.user")
~database:(Helm_registry.get "db.database")
()
-let _ = MetadataDb.clean ~dbd ~owner:(Helm_registry.get "matita.owner")
+
+let owner = (Helm_registry.get "matita.owner") ;;
+let _ = MetadataTypes.ownerize_tables owner ;;
+let _ = MatitaDb.clean_owner_environment dbd owner ;;
+let _ = MatitaDb.create_owner_environment dbd owner ;;
+
let disambiguator =
new MatitaDisambiguator.disambiguator ~parserr ~dbd
~chooseUris:mono_uris_callback ~chooseInterp:mono_interp_callback
()
let console = new tty_console
-let currentProof = (new MatitaProof.currentProof :> MatitaTypes.currentProof)
-let interpreter =
- new MatitaInterpreter.interpreter
- ~disambiguator ~currentProof ~console ~dbd ()
+let interpreter = MatitaInterpreter.interpreter ~disambiguator ~console ()
let run_script fname =
message (sprintf "execution of %s started:" fname);
let script =
let ic = open_in fname in
- let ast = snd (CicTextualParser2.parse_script (Stream.of_channel ic)) in
+ let ast =
+ try
+ snd (CicTextualParser2.parse_script (Stream.of_channel ic))
+ with
+ exn ->
+ error (explain exn);
+ assert false (* should be something like (Unix.exit 1) *)
+ in
close_in ic;
ast
in