X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatitac.ml;h=533bbc6a3d46df166290596df4da29ed2a745ae4;hb=fdd8107cc53f5e862004aa5fcd48593ee5634234;hp=64870249019b5e8e79ef29f062870bf5504d4584;hpb=ac813b7e251e4bac1a8a16befa628203775771ca;p=helm.git

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index 648702490..533bbc6a3 100644
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -46,6 +46,8 @@ class tty_console =
       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} *)
@@ -57,7 +59,12 @@ let usage =
   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
@@ -65,34 +72,26 @@ let scripts =
   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 =
@@ -107,7 +106,8 @@ let run_script fname =
         else
           aux tl
   in
-  aux script
+  aux script;
+  message (sprintf "execution of %s completed." fname)
 
 let _ = List.iter run_script scripts