better owner hadling

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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 40f2077cfccb3f8a0f8d1f4a0061cab7e859a79d..bc42bba543676965d535706552c80dcf749fcd1d 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -43,7 +43,12 @@ let dbd =
     ~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 gui = MatitaGui.instance ()
 let disambiguator =
   new MatitaDisambiguator.disambiguator ~parserr ~dbd
@@ -51,7 +56,11 @@ let disambiguator =
     ~chooseInterp:(interactive_interp_choice ~gui)
     ()
 
+let currentProof = new MatitaProof.currentProof
+
 let currentProof = MatitaProof.instance ()
+
+
 let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
 let sequents_viewer =
   let set_goal goal =