From f3cc1fe99d45cf1f473226d91df36118db638db5 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi 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 : mostra il tipo dell'oggetto indicato non riconosce tipi induttivi e prove incomplete -levels : mostra l'attribuzione dei livelli - -locate : invocazione di Locate + -restricted : non usa il db: vanno solo -d -t -l + -locate : invocazione di Locate -backward : invocazione di Backward -mbackward : invoca le Backward con indice da 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 ^ "

"); 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