snapshot, notably:

[helm.git] / helm / matita / matitac.ml

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index c29b507792f698035809c66bd055827b85e4044b..2ae1c8d6846b635d1dca96a10121bb4ef0224969 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -57,7 +57,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,25 +70,8 @@ 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 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 interpreter = MatitaInterpreter.interpreter ~disambiguator ~console ()
+let interpreter = MatitaInterpreter.interpreter ~console ()
 
 let run_script fname =
   message (sprintf "execution of %s started:" fname);