topLevel updated to use mqint set_database and get_database

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index cc1b3034bef986fc3b50d16f60b3a83e01aa0015..d53ea70eaf5096cb4a015266a0d58fa958bca7c9 100644 (file)
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -49,9 +49,23 @@ let pp_type_of uri =
 *)
    in print_endline s; flush stdout
 
+let set_dbms i =
+   if i = 1 then Mqint.set_database Mqint.postgres_db else
+   if i = 2 then Mqint.set_database Mqint.galax_db else ()
+   
+let get_dbms s =
+   if s = Mqint.postgres_db then 1 else
+   if s = Mqint.galax_db then 2 else 0
+
 let dbc () =
    let on = check_db () in 
-   if on then ignore (Mqint.check ())
+   if on then
+   begin
+      let dbms = Mqint.get_database () in
+      prerr_endline ("toplevel: current dbms is n." ^ 
+                     string_of_int (get_dbms dbms) ^ " (" ^ dbms ^ ")");
+      Mqint.check ()
+   end
 
 let rec display = function
    | []           -> ()
@@ -138,6 +152,7 @@ let prerr_help () =
    prerr_endline "-q  -show-queries       outputs generated queries";
    prerr_endline "-s  -stat               outputs interpreter statistics";
    prerr_endline "-c  -db-check           checks the database connection";
+   prerr_endline "-i  -interpreter NUMBER sets the dbms to be used (default 1)";
    prerr_endline "-r  -restricted -nodb   enables restricted mode: queries are not issued";
    prerr_endline "-t  -typeof URI         outputs the CIC type of the given HELM object";
    prerr_endline "-x  -execute            issues a query given in the input file";
@@ -148,7 +163,8 @@ let prerr_help () =
    prerr_endline "                        in the input file";
    prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0 on all";
    prerr_endline "                        CIC terms in the input file\n";
-   prerr_endline "NOTES: CIC terms are read with the HELM CIC Textual Parser";
+   prerr_endline "NOTES: interpreter numbers are 1 for postgres and 2 for galax";
+   prerr_endline "       CIC terms are read with the HELM CIC Textual Parser";
    prerr_endline "       -typeof does not work with inductive types and proofs in progress\n"
 
 let parse_args () =
@@ -162,6 +178,7 @@ let parse_args () =
       | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
       | ("-s"|"-stat") :: rem -> Mqint.set_stat true; parse rem
       | ("-r"|"-restricted"|"-nodb") :: rem -> use_db := false; parse rem
+      | ("-i"|"-interpreter") :: dbms :: rem -> set_dbms (int_of_string dbms); parse rem
       | ("-c"|"-db-check") :: rem -> dbc (); parse rem
       | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
       | ("-B"|"-backward") :: arg :: rem ->
@@ -182,6 +199,7 @@ let _ =
       ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
    Mqint.set_stat false;
    Gen.set_log_file "MQGenLog.htm";
+   set_dbms 1;
    parse_args ();
    if not ! db_down then Mqint.close ();
    Gen.set_confirm_query (fun _ -> true);