with exn ->
self#echo_error (explain exn);
None
+ method show ?(msg = "") () = assert false; ()
+ method choose_uri (uris: string list): string = assert false
end
(** {2 Initialization} *)
sprintf "MatitaC v%s\nUsage: matitac [option ...] file ...\nOptions:"
BuildTimeConf.version
-let _ = Helm_registry.load_from "matita.conf.xml"
+let _ =
+ Helm_registry.load_from "matita.conf.xml";
+ Http_getter.init ();
+ MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+ MatitaDb.clean_owner_environment ();
+ MatitaDb.create_owner_environment ()
let scripts =
let acc = ref [] in
Arg.parse arg_spec add_script usage;
List.rev !acc
-let parserr = new MatitaDisambiguator.parserr ()
-let dbd =
- Mysql.quick_connect
- ~host:(Helm_registry.get "db.host")
- ~user:(Helm_registry.get "db.user")
- ~database:(Helm_registry.get "db.database")
- ()
-let _ = MetadataDb.clean ~dbd ~owner:(Helm_registry.get "matita.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 ~console ()
let run_script fname =
- message (sprintf "execution of %s started." 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
let rec aux = function
- | [] -> ()
+ | [] -> () (* script is over *)
| DisambiguateTypes.Comment _ :: tl -> aux tl
| DisambiguateTypes.Command ast :: tl ->
let loc =
else
aux tl
in
- aux script
+ aux script;
+ message (sprintf "execution of %s completed." fname)
let _ = List.iter run_script scripts