+let connection_param = "host=mowgli.cs.unibo.it dbname=helm user=helm"
+
let show_queries = ref false
let use_db = ref true
let check_db () =
if ! db_down then
- if ! use_db then begin Mqint.init (); db_down := false; true end
+ if ! use_db then begin Mqint.init connection_param; db_down := false; true end
else begin print_endline "Not issuing in restricted mode"; false end
else true
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
*)
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 ->
| [] -> ()
| term :: tail ->
backward level tail;
- print_string ("? " ^ CicPp.ppterm term ^ nl);
try
+ if Mqint.get_stat () then
+ print_string ("? " ^ CicPp.ppterm term ^ nl);
let t0 = Sys.time () in
let r = Gen.backward [] [] term level in
let t1 = Sys.time () -. t0 in
- let info = List.nth (Gen.get_query_info ()) 0 in
- print_string ("GEN = " ^ info ^ ":" ^ string_of_float t1 ^ "s" ^ nl);
+ let info = Gen.get_query_info () in
+ let num = List.nth info 0 in
+ let gen = List.nth info 1 in
+ if Mqint.get_stat () then
+ print_string (num ^ " GEN = " ^ gen ^ ":" ^ string_of_float t1 ^ "s" ^ nl);
print_string (Util.text_of_result r nl);
flush stdout
with Gen.Discard -> ()
prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n";
prerr_endline "OPTIONS:\n";
prerr_endline "-h -help shows this help message";
- prerr_endline "-q -show-queries outputs the generated queries";
+ prerr_endline "-q -show-queries outputs generated queries";
+ prerr_endline "-s -stat outputs interpreter statistics";
+ 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";
| ("-l"|"-levels") :: rem -> levels (get_terms ())
| ("-x"|"-execute") :: rem -> execute stdin; parse rem
| ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
+ | ("-s"|"-stat") :: rem -> Mqint.set_stat 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
Logger.log_callback :=
(Logger.log_to_html
~print_and_flush:(function s -> print_string s ; flush stdout)) ;
+ Mqint.set_stat false;
Gen.set_log_file "MQGenLog.htm";
parse_args ();
if not ! db_down then Mqint.close ();