claude

src/manager/db.ml

@@ -10,10 +10,15 @@ type handle = {
   mode: transaction_mode;
 }
 
-(*
-let raw db = db.raw_db
-*)
-  
+let current_db = ref None
+ 
+let current () = 
+  match !current_db with
+    | None -> failwith "Db.current: database not yet initialized"
+    | Some x -> x
+
+	      
+
 let default_busyfn (db:Sqlite3.db) =
   print_endline "WARNING: busy";
   (* Thread.delay (Random.float 1.) *)
@@ -1011,22 +1016,22 @@ module Transf = struct
 end
 
 
-
-
-let create ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
-  let db = {
-    raw_db = Sqlite3.db_open db_name; 
-    in_transaction = 0; 
-    mode = mode; 
-    busyfn = busyfn } 
-  in
-  Loc.init db;
-  (*
-    External_proof.init db;
-    Goal.init db;
-    Transf.init db;
-  *)
-  db
+let init_db ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
+  match !current_db with
+    | None ->
+	current_db <- Some {
+	  raw_db = Sqlite3.db_open db_name; 
+	  in_transaction = 0; 
+	  mode = mode; 
+	  busyfn = busyfn } 
+	in
+	Loc.init db;
+	(*
+	  External_proof.init db;
+	  Goal.init db;
+	  Transf.init db;
+	*)
+	db
 
 
 exception AlreadyAttempted

src/manager/db.mli

@@ -2,8 +2,7 @@
 
 (** {1 Proof manager database} *)
 
-(** {2 The persistent database} *)
-
+(*
 type handle
   (** Database handle which can be used to create and retrieve objects *)
 
@@ -24,7 +23,7 @@ val raw: handle -> Sqlite3.db
   (** [raw db] @return the underlying Sqlite3 database for the
       connection, for advanced queries.  *)
 *)
-
+*)
 
 
 
@@ -121,8 +120,15 @@ val transf_obsolete :  transf -> bool
 val subgoals : transf -> goal list
 
 
-val read_db_from_file : string -> goal list
-(** returns the set of root goals *)
+(** {2 The persistent database} *)
+
+val init_base : string -> unit
+(** opens or creates the current database, from given file name *)
+
+val root_goals : unit -> goal list
+(** returns the current set of root goals *)
+
+
 
 (** {2 attempts to solve goals} *)