quiet_mode;
authorwenzelm
Wed Apr 14 19:07:39 1999 +0200 (1999-04-14)
changeset 6432cdde45202c5c
parent 6431 a42bdc45130d
child 6433 228237ec56e5
quiet_mode;
TFL/post.sml
     1.1 --- a/TFL/post.sml	Wed Apr 14 19:07:04 1999 +0200
     1.2 +++ b/TFL/post.sml	Wed Apr 14 19:07:39 1999 +0200
     1.3 @@ -9,6 +9,8 @@
     1.4  signature TFL = 
     1.5    sig
     1.6     structure Prim : TFL_sig
     1.7 +   val quiet_mode : bool ref
     1.8 +   val message : string -> unit
     1.9  
    1.10     val tgoalw : theory -> thm list -> thm list -> thm list
    1.11     val tgoal: theory -> thm list -> thm list
    1.12 @@ -40,6 +42,13 @@
    1.13   structure Prim = Prim
    1.14   structure S = USyntax
    1.15  
    1.16 +
    1.17 +(* messages *)
    1.18 +
    1.19 +val quiet_mode = ref false;
    1.20 +fun message s = if ! quiet_mode then () else writeln s;
    1.21 +
    1.22 +
    1.23  (*---------------------------------------------------------------------------
    1.24   * Extract termination goals so that they can be put it into a goalstack, or 
    1.25   * have a tactic directly applied to them.
    1.26 @@ -138,16 +147,16 @@
    1.27    val gen_all = S.gen_all
    1.28  in
    1.29  fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} =
    1.30 -  let val dummy = writeln "Proving induction theorem..  "
    1.31 +  let val dummy = message "Proving induction theorem..  "
    1.32        val ind = Prim.mk_induction theory f R full_pats_TCs
    1.33 -      val dummy = writeln "Proved induction theorem.\nPostprocessing..  "
    1.34 +      val dummy = message "Proved induction theorem.\nPostprocessing..  "
    1.35        val {rules, induction, nested_tcs} = 
    1.36  	  std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs}
    1.37    in
    1.38    case nested_tcs
    1.39 -  of [] => (writeln "Postprocessing done.";
    1.40 +  of [] => (message "Postprocessing done.";
    1.41              {induction=induction, rules=rules,tcs=[]})
    1.42 -  | L  => let val dummy = writeln "Simplifying nested TCs..  "
    1.43 +  | L  => let val dummy = message "Simplifying nested TCs..  "
    1.44                val (solved,simplified,stubborn) =
    1.45                 U.itlist (fn th => fn (So,Si,St) =>
    1.46                       if (id_thm th) then (So, Si, th::St) else
    1.47 @@ -157,7 +166,7 @@
    1.48                val rewr = full_simplify (ss addsimps (solved @ simplified'));
    1.49                val induction' = rewr induction
    1.50                and rules'     = rewr rules
    1.51 -              val dummy = writeln "Postprocessing done."
    1.52 +              val dummy = message "Postprocessing done."
    1.53            in
    1.54            {induction = induction',
    1.55                 rules = rules',
    1.56 @@ -232,13 +241,13 @@
    1.57  local structure R = Rules
    1.58  in
    1.59  fun function theory eqs = 
    1.60 - let val dummy = writeln "Making definition..   "
    1.61 + let val dummy = message "Making definition..   "
    1.62       val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs
    1.63       val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules))
    1.64 -     val dummy = writeln "Definition made."
    1.65 -     val dummy = writeln "Proving induction theorem..  "
    1.66 +     val dummy = message "Definition made."
    1.67 +     val dummy = message "Proving induction theorem..  "
    1.68       val induction = Prim.mk_induction theory f R full_pats_TCs
    1.69 -     val dummy = writeln "Induction theorem proved."
    1.70 +     val dummy = message "Induction theorem proved."
    1.71   in {theory = theory, 
    1.72       eq_ind = standard (induction RS (rules RS conjI))}
    1.73   end