tuned;
authorwenzelm
Sat Jan 24 21:37:31 2015 +0100 (2015-01-24 ago)
changeset 5943242b7b76b37b8
parent 59431 db440f97cf1a
child 59433 9da5b2c61049
tuned;
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jan 24 21:36:21 2015 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Jan 24 21:37:31 2015 +0100
     1.3 @@ -212,7 +212,7 @@
     1.4    | has_tfree_syntactic_sort _ = false
     1.5  val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort)
     1.6  
     1.7 -fun plazy f = Pretty.blk (0, pstrs (f ()))
     1.8 +fun plazy f = Pretty.para (f ())
     1.9  
    1.10  fun pick_them_nits_in_term deadline state (params : params) mode i n step
    1.11                             subst def_assm_ts nondef_assm_ts orig_t =
    1.12 @@ -245,7 +245,7 @@
    1.13      fun pprint_nt f = () |> is_mode_nt mode ? pprint writeln o f
    1.14      fun pprint_v f = () |> verbose ? pprint writeln o f
    1.15      fun pprint_d f = () |> debug ? pprint tracing o f
    1.16 -    val print = pprint writeln o curry Pretty.blk 0 o pstrs
    1.17 +    val print = pprint writeln o Pretty.para
    1.18      fun print_t f = () |> mode = TPTP ? print o f
    1.19  (*
    1.20      val print_g = pprint tracing o Pretty.str
    1.21 @@ -330,9 +330,9 @@
    1.22  
    1.23      fun print_wf (x, (gfp, wf)) =
    1.24        pprint_nt (fn () => Pretty.blk (0,
    1.25 -          pstrs ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")
    1.26 +          Pretty.text ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")
    1.27            @ Syntax.pretty_term ctxt (Const x) ::
    1.28 -          pstrs (if wf then
    1.29 +          Pretty.text (if wf then
    1.30                     "\" was proved well-founded. Nitpick can compute it \
    1.31                     \efficiently."
    1.32                   else
    1.33 @@ -367,9 +367,9 @@
    1.34      fun monotonicity_message Ts extra =
    1.35        let val pretties = map (pretty_maybe_quote keywords o pretty_for_type ctxt) Ts in
    1.36          Pretty.blk (0,
    1.37 -          pstrs ("The type" ^ plural_s_for_list pretties ^ " ") @
    1.38 +          Pretty.text ("The type" ^ plural_s_for_list pretties ^ " ") @
    1.39            pretty_serial_commas "and" pretties @
    1.40 -          pstrs (" " ^
    1.41 +          Pretty.text (" " ^
    1.42                   (if none_true monos then
    1.43                      "passed the monotonicity test"
    1.44                    else
    1.45 @@ -657,14 +657,14 @@
    1.46        in
    1.47          (pprint_a (Pretty.chunks
    1.48               [Pretty.blk (0,
    1.49 -                  (pstrs ((if mode = Auto_Try then "Auto " else "") ^
    1.50 +                  (Pretty.text ((if mode = Auto_Try then "Auto " else "") ^
    1.51                            "Nitpick found a" ^
    1.52                            (if not genuine then " potentially spurious "
    1.53                             else if genuine_means_genuine then " "
    1.54                             else " quasi genuine ") ^ das_wort_model) @
    1.55                     (case pretties_for_scope scope verbose of
    1.56                        [] => []
    1.57 -                    | pretties => pstrs " for " @ pretties) @
    1.58 +                    | pretties => Pretty.text " for " @ pretties) @
    1.59                     [Pretty.str ":", Pretty.fbrk])),
    1.60                Pretty.indent indent_size reconstructed_model]);
    1.61           print_t (K "% SZS output end FiniteModel");
    1.62 @@ -863,7 +863,7 @@
    1.63            else if verbose then
    1.64              pprint_nt (fn () => Pretty.chunks
    1.65                  [Pretty.blk (0,
    1.66 -                     pstrs ((if n > 1 then
    1.67 +                     Pretty.text ((if n > 1 then
    1.68                                 "Batch " ^ string_of_int (j + 1) ^ " of " ^
    1.69                                 signed_string_of_int n ^ ": "
    1.70                               else
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Jan 24 21:36:21 2015 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sat Jan 24 21:37:31 2015 +0100
     2.3 @@ -70,7 +70,6 @@
     2.4    val eta_expand : typ list -> term -> int -> term
     2.5    val DETERM_TIMEOUT : Time.time -> tactic -> tactic
     2.6    val indent_size : int
     2.7 -  val pstrs : string -> Pretty.T list
     2.8    val unyxml : string -> string
     2.9    val pretty_maybe_quote : Keyword.keywords -> Pretty.T -> Pretty.T
    2.10    val hash_term : term -> int
    2.11 @@ -281,8 +280,6 @@
    2.12  
    2.13  val indent_size = 2
    2.14  
    2.15 -val pstrs = Pretty.breaks o map Pretty.str o space_explode " "
    2.16 -
    2.17  val unyxml = ATP_Util.unyxml
    2.18  
    2.19  val maybe_quote = ATP_Util.maybe_quote