From: Stefano Zacchiroli 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