src/HOL/Tools/Nitpick/nitpick.ML
changeset 58843 521cea5fa777
parent 57996 ca917ea6969c
child 58892 20aa19ecf2cc
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Oct 31 11:18:17 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Oct 31 11:36:41 2014 +0100
     1.3 @@ -241,11 +241,11 @@
     1.4          o Pretty.mark Markup.information
     1.5        else
     1.6          print o Pretty.string_of
     1.7 -    val pprint_a = pprint Output.urgent_message
     1.8 -    fun pprint_nt f = () |> is_mode_nt mode ? pprint Output.urgent_message o f
     1.9 -    fun pprint_v f = () |> verbose ? pprint Output.urgent_message o f
    1.10 +    val pprint_a = pprint writeln
    1.11 +    fun pprint_nt f = () |> is_mode_nt mode ? pprint writeln o f
    1.12 +    fun pprint_v f = () |> verbose ? pprint writeln o f
    1.13      fun pprint_d f = () |> debug ? pprint tracing o f
    1.14 -    val print = pprint Output.urgent_message o curry Pretty.blk 0 o pstrs
    1.15 +    val print = pprint writeln o curry Pretty.blk 0 o pstrs
    1.16      fun print_t f = () |> mode = TPTP ? print o f
    1.17  (*
    1.18      val print_g = pprint tracing o Pretty.str
    1.19 @@ -1015,8 +1015,8 @@
    1.20  fun pick_nits_in_term state (params as {timeout, expect, ...}) mode i n step
    1.21                        subst def_assm_ts nondef_assm_ts orig_t =
    1.22    let
    1.23 -    val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
    1.24 -    val print_t = if mode = TPTP then Output.urgent_message else K ()
    1.25 +    val print_nt = if is_mode_nt mode then writeln else K ()
    1.26 +    val print_t = if mode = TPTP then writeln else K ()
    1.27    in
    1.28      if getenv "KODKODI" = "" then
    1.29        (* The "expect" argument is deliberately ignored if Kodkodi is missing so
    1.30 @@ -1068,7 +1068,7 @@
    1.31      val t = state |> Proof.raw_goal |> #goal |> prop_of
    1.32    in
    1.33      case Logic.count_prems t of
    1.34 -      0 => (Output.urgent_message "No subgoal!"; (noneN, state))
    1.35 +      0 => (writeln "No subgoal!"; (noneN, state))
    1.36      | n =>
    1.37        let
    1.38          val t = Logic.goal_params t i |> fst