From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 15 Oct 2002 15:57:15 +0000 (+0000)
Subject: added -s switch and query numeration
X-Git-Tag: new_mathql_before_first_merge~5
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7b0f1b37acba240d7a5d6847e3d8e46b19ce676c;p=helm.git

added -s switch and query numeration
---

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index 16d28dc01..cc1b3034b 100644
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -103,13 +103,17 @@ let mbackward n m l =
       | []           -> ()
       | 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 -> ()
@@ -131,7 +135,8 @@ let prerr_help () =
    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";
@@ -155,6 +160,7 @@ let parse_args () =
       | ("-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
@@ -174,6 +180,7 @@ let _ =
    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 ();