verbose flag;
authorwenzelm
Tue Apr 27 15:13:18 1999 +0200 (1999-04-27)
changeset 6528ed8c5f738ab3
parent 6527 f7a7ac2b9926
child 6529 0f4c2ebc5018
verbose flag;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Apr 27 15:12:34 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Apr 27 15:13:18 1999 +0200
     1.3 @@ -9,15 +9,13 @@
     1.4    - smash_unifiers: ever invents new vars (???);
     1.5  *)
     1.6  
     1.7 -(* FIXME tmp *)
     1.8 -val proof_debug = ref false;
     1.9 -
    1.10  signature PROOF_CONTEXT =
    1.11  sig
    1.12    type context
    1.13    exception CONTEXT of string * context
    1.14    val theory_of: context -> theory
    1.15    val sign_of: context -> Sign.sg
    1.16 +  val verbose: bool ref
    1.17    val print_binds: context -> unit
    1.18    val print_thms: context -> unit
    1.19    val print_context: context -> unit
    1.20 @@ -108,8 +106,8 @@
    1.21  
    1.22  (** print context information **)
    1.23  
    1.24 -(* FIXME tmp*)
    1.25 -fun debug f x = if ! proof_debug then f x else ();
    1.26 +val verbose = ref false;
    1.27 +fun verb f x = if ! verbose then f x else ();
    1.28  
    1.29  fun print_items prt name items =
    1.30    let
    1.31 @@ -170,15 +168,15 @@
    1.32      val prt_defT = prt_atom prt_var prt_typ;
    1.33      val prt_defS = prt_atom prt_varT prt_sort;
    1.34    in
    1.35 -    debug Pretty.writeln pretty_thy;
    1.36 +    verb Pretty.writeln pretty_thy;
    1.37      Pretty.writeln (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes)));
    1.38      print_items (prt_term o #prop o Thm.rep_thm) "Assumptions:" assumes;
    1.39 -    debug print_binds ctxt;
    1.40 -    debug print_thms ctxt;
    1.41 -    debug Pretty.writeln (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types)));
    1.42 -    debug Pretty.writeln (Pretty.big_list "Default sorts:" (map prt_defS (Vartab.dest sorts)));
    1.43 -    debug writeln ("Maxidx: " ^ string_of_int maxidx);
    1.44 -    debug Pretty.writeln (Pretty.strs ("Used type variable names:" :: used))
    1.45 +    verb print_binds ctxt;
    1.46 +    verb print_thms ctxt;
    1.47 +    verb Pretty.writeln (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types)));
    1.48 +    verb Pretty.writeln (Pretty.big_list "Default sorts:" (map prt_defS (Vartab.dest sorts)));
    1.49 +    verb writeln ("Maxidx: " ^ string_of_int maxidx);
    1.50 +    verb Pretty.writeln (Pretty.strs ("Used type variable names:" :: used))
    1.51    end;
    1.52  
    1.53