From f3cc1fe99d45cf1f473226d91df36118db638db5 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 13 Sep 2002 16:52:32 +0000
Subject: [PATCH] restricted mode to use when the database is down :)

---
 helm/gTopLevel/topLevel/Readme      |  5 +++--
 helm/gTopLevel/topLevel/topLevel.ml | 22 ++++++++++++++++++----
 2 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/helm/gTopLevel/topLevel/Readme b/helm/gTopLevel/topLevel/Readme
index 1607e5d83..9f0feb769 100644
--- 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 7736c1a29..9992e4093 100644
--- 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
-- 
2.39.2