From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Sat, 24 Jan 2004 12:29:26 +0000 (+0000)
Subject: - quiet debugging for mathql
X-Git-Tag: V_0_2_3~154
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8c1d14fa9110ec0d42b17d2279c0d0cfe7865a52;p=helm.git

- quiet debugging for mathql
- defined a debug_print function with a verbosity level
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 8932d21a8..c3ef122db 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -33,7 +33,10 @@
 (*                                                                            *)
 (******************************************************************************)
 
-open Printf;;
+let debug_level = ref 1
+let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s
+
+open Printf
 
 (* DEBUGGING *)
 
@@ -45,11 +48,9 @@ module MQG  = MQueryGenerator
 
 (* GLOBAL CONSTANTS *)
 
-let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
-(*
-let mqi_flags = [] (* default MathQL interpreter options *)
-*)
-let mqi_handle = MQIC.init mqi_flags prerr_string
+let mqi_debug_fun s = debug_print ~level:2 s
+let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log]
+let mqi_handle = MQIC.init mqi_flags mqi_debug_fun
 
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
 
@@ -572,8 +573,8 @@ let refresh_proof (output : TermViewer.proof_viewer) =
  match ProofEngine.get_proof () with
     None -> assert false
   | Some (uri,metasenv,bo,ty) ->
-prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
-   raise (InvokeTactics.RefreshProofException e)
+      debug_print ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[])));
+      raise (InvokeTactics.RefreshProofException e)
 
 let set_proof_engine_goal g =
  ProofEngine.goal := g
@@ -633,10 +634,13 @@ let metasenv =
   | Some (_,metasenv,_,_) -> metasenv
 in
 try
-let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
-   prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
-      raise (InvokeTactics.RefreshSequentException e)
-with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e)
+  let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
+  debug_print
+    ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent);
+  raise (InvokeTactics.RefreshSequentException e)
+with Not_found ->
+  debug_print ("Offending sequent " ^ string_of_int metano ^ " unknown.");
+  raise (InvokeTactics.RefreshSequentException e)
 
 module InvokeTacticsCallbacks =
  struct
@@ -1379,13 +1383,13 @@ let new_inductive () =
      let obj = Cic.InductiveDefinition(tys,params,!paramsno) in
       begin
        try
-        prerr_endline (CicPp.ppobj obj) ;
+        debug_print (CicPp.ppobj obj);
         CicTypeChecker.typecheck_mutual_inductive_defs uri
          (tys,params,!paramsno) ;
         with
          e ->
-          prerr_endline "Offending mutual (co)inductive type declaration:" ;
-          prerr_endline (CicPp.ppobj obj) ;
+          debug_print "Offending mutual (co)inductive type declaration:" ;
+          debug_print (CicPp.ppobj obj) ;
       end ;
       (* We already know that obj is well-typed. We need to add it to the  *)
       (* environment in order to compute the inner-types without having to *)
@@ -2106,7 +2110,7 @@ let choose_selection mmlwidget (element : Gdome.element option) =
        | Some p -> aux (new Gdome.element_of_node p)
     with
        GdomeInit.DOMCastException _ ->
-        prerr_endline
+        debug_print
          "******* trying to select above the document root ********"
   in
    match element with