src/HOL/Tools/Nitpick/nitpick.ML
changeset 46086 096697aec8a7
parent 45666 d83797ef0d2d
child 46103 1e35730bd869
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jan 03 18:33:17 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Jan 03 18:33:18 2012 +0100
     1.3 @@ -235,20 +235,19 @@
     1.4           show_skolems, show_consts, evals, formats, atomss, max_potential,
     1.5           max_genuine, check_potential, check_genuine, batch_size, ...} = params
     1.6      val state_ref = Unsynchronized.ref state
     1.7 -    val pprint =
     1.8 +    fun pprint print =
     1.9        if mode = Auto_Try then
    1.10          Unsynchronized.change state_ref o Proof.goal_message o K
    1.11          o Pretty.chunks o cons (Pretty.str "") o single
    1.12          o Pretty.mark Isabelle_Markup.hilite
    1.13        else
    1.14 -        (fn s => (Output.urgent_message s; if debug then tracing s else ()))
    1.15 -        o Pretty.string_of
    1.16 -    fun pprint_n f = () |> mode = Normal ? pprint o f
    1.17 -    fun pprint_v f = () |> verbose ? pprint o f
    1.18 -    fun pprint_d f = () |> debug ? pprint o f
    1.19 -    val print = pprint o curry Pretty.blk 0 o pstrs
    1.20 +        print o Pretty.string_of
    1.21 +    fun pprint_n f = () |> mode = Normal ? pprint Output.urgent_message o f
    1.22 +    fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f
    1.23 +    fun pprint_d f = () |> debug ? pprint tracing o f
    1.24 +    val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs
    1.25  (*
    1.26 -    val print_g = pprint o Pretty.str
    1.27 +    val print_g = pprint tracing o Pretty.str
    1.28  *)
    1.29      val print_n = pprint_n o K o plazy
    1.30      val print_v = pprint_v o K o plazy
    1.31 @@ -323,7 +322,7 @@
    1.32        got_all_mono_user_axioms andalso no_poly_user_axioms
    1.33  
    1.34      fun print_wf (x, (gfp, wf)) =
    1.35 -      pprint (Pretty.blk (0,
    1.36 +      pprint_n (fn () => Pretty.blk (0,
    1.37            pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")
    1.38            @ Syntax.pretty_term ctxt (Const x) ::
    1.39            pstrs (if wf then
    1.40 @@ -672,7 +671,7 @@
    1.41            codatatypes_ok
    1.42          fun assms_prop () = Logic.mk_conjunction_list (neg_t :: assm_ts)
    1.43        in
    1.44 -        (pprint (Pretty.chunks
    1.45 +        (pprint_n (fn () => Pretty.chunks
    1.46               [Pretty.blk (0,
    1.47                    (pstrs ((if mode = Auto_Try then "Auto " else "") ^
    1.48                            "Nitpick found a" ^
    1.49 @@ -881,7 +880,7 @@
    1.50            if null scopes then
    1.51              print_n (K "The scope specification is inconsistent.")
    1.52            else if verbose then
    1.53 -            pprint (Pretty.chunks
    1.54 +            pprint_n (fn () => Pretty.chunks
    1.55                  [Pretty.blk (0,
    1.56                       pstrs ((if n > 1 then
    1.57                                 "Batch " ^ string_of_int (j + 1) ^ " of " ^