restricted mode to use when the database is down :)

diff --git a/helm/gTopLevel/topLevel/Readme b/helm/gTopLevel/topLevel/Readme
index 1607e5d835a87ec8598f27ec1b9570d71d19e63c..9f0feb7696d2220de5d86bd4339e0a03d7fbdd5c 100644 (file)
--- a/helm/gTopLevel/topLevel/Readme
+++ b/helm/gTopLevel/topLevel/Readme
@@ -10,8 +10,9 @@ Opzioni : -display            : mostra solo i termini CIC nell'input
           -typeof <URI>       : mostra il tipo dell'oggetto indicato
                                non riconosce tipi induttivi e prove incomplete
           -levels <indice>    : mostra l'attribuzione dei livelli
-          -locate <nome>      : invocazione di Locate
+          -restricted         : non usa il db: vanno solo -d -t -l 
+         -locate <nome>      : invocazione di Locate
           -backward <indice>  : invocazione di Backward
          -mbackward <indice> : invoca le Backward con indice da <indice> a 0
 
-le opzioni si possono anche scrivere -d -t -l -L -B e -MB nell'ordine.
+le opzioni si possono anche scrivere -d -t -l -r -L -B e -MB nell'ordine.

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index 7736c1a29404b17ea0f194e0c5e0250d74cccf97..9992e409369e8c33de911cc622840b8615c376a2 100644 (file)
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -1,3 +1,15 @@
+let use_db = ref true
+
+let db_down = ref true
+
+let check_db () =
+   if ! db_down then begin
+      if ! use_db then begin 
+         MQueryGenerator.init (); db_down := false
+      end else
+        raise (Failure "Operation impossible in restricted mode")
+   end
+      
 let get_terms () =
    let terms = ref [] in
    let lexbuf = Lexing.from_channel stdin in
@@ -27,7 +39,8 @@ let pp_type_of uri =
 *)
    in print_endline s; flush stdout
 
-let locate name = 
+let locate name =
+   check_db ();
    print_endline (MQueryGenerator.locate_html name);
    flush stdout
 
@@ -45,7 +58,7 @@ let rec levels = function
       print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
       print_endline (MQueryGenerator.levels [] [] term);
       flush stdout
-
+   
 let mbackward n m l =
    let queries = ref [] in
    let issue query = 
@@ -60,6 +73,7 @@ let mbackward n m l =
          print_endline (MQueryGenerator.backward [] [] term level);
          flush stdout
    in
+   check_db ();
    MQueryGenerator.call_back issue;
    for level = max m n downto min m n do
       prerr_endline ("toplevel: backward: trying level " ^
@@ -77,6 +91,7 @@ let parse_args () =
       | ("-d"|"-display") :: rem -> display (get_terms ())
       | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
       | ("-l"|"-levels") :: rem -> levels (get_terms ())
+      | ("-r"|"-restricted") :: rem -> use_db := false; parse rem
       | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem
       | ("-B"|"-backward") :: arg :: rem ->
          let m = (int_of_string arg) in
@@ -93,9 +108,8 @@ let _ =
    Logger.log_callback :=
       (Logger.log_to_html
       ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
-   MQueryGenerator.init ();
    parse_args ();
-   MQueryGenerator.close ();
+   if not ! db_down then MQueryGenerator.close ();
    prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^
                   " seconds");
    exit 0