From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 3 Oct 2002 15:06:50 +0000 (+0000)
Subject: toplevel updated
X-Git-Tag: new_mathql_before_first_merge~18
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6fbae5ce3e80b90ce3f30f43fb8f4bd35043c51d;p=helm.git

toplevel updated
---

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index 57c9d41bf..4c202a6d5 100644
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -15,7 +15,8 @@ let check_db () =
 let default_confirm q =
    let module Util = MQueryUtil in   
    if ! show_queries then print_string (Util.text_of_query q ^ nl);
-   check_db ()
+   let b = check_db () in
+   if ! db_down then print_endline "db_down"; b 
 
 let get_terms () =
    let terms = ref [] in
@@ -46,6 +47,10 @@ let pp_type_of uri =
 *)
    in print_endline s; flush stdout
 
+let dbc () =
+   let on = check_db () in 
+   if on then ignore (Mqint.check ())
+
 let rec display = function
    | []           -> ()
    | term :: tail -> 
@@ -125,6 +130,7 @@ let prerr_help () =
    prerr_endline "OPTIONS:\n";
    prerr_endline "-h  -help               shows this help message";
    prerr_endline "-q  -show-queries       outputs the generated queries";
+   prerr_endline "-c  -db-check           checks the database connection";
    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,6 +154,7 @@ let parse_args () =
       | ("-x"|"-execute") :: rem -> execute stdin; parse rem
       | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
       | ("-r"|"-restricted"|"-nodb") :: rem -> use_db := false; parse rem
+      | ("-c"|"-db-check") :: rem -> dbc (); parse rem
       | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
       | ("-B"|"-backward") :: arg :: rem ->
          let m = (int_of_string arg) in