+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
*)
in print_endline s; flush stdout
-let locate name =
- print_endline (MQueryGenerator.locate name);
+let locate name =
+ check_db ();
+ print_endline (snd (MQueryGenerator.locate name)) ;
flush stdout
let rec display = 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 =
| term :: tail ->
backward level tail;
print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
- print_endline (MQueryGenerator.backward [] [] term level);
+ print_endline (snd (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 " ^
| ("-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
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