# HG changeset patch # User wenzelm # Date 1428789304 -7200 # Node ID fe31c7e7ebf4f84640d63154e6da7d2a3c7d163d # Parent 69e7fe18b7db43c3967e62008d40a68259c5cd5b# Parent f3e70d74a686427be2843cd5ae069f13c2403b00 merged diff -r 69e7fe18b7db -r fe31c7e7ebf4 src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML Sat Apr 11 22:19:09 2015 +0100 +++ b/src/HOL/Library/code_test.ML Sat Apr 11 23:55:04 2015 +0200 @@ -148,7 +148,8 @@ (ts ~~ evals))] fun pretty_failure ctxt target (((_, evals), query), eval_ts) = - Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] + Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") + @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)] @ pretty_eval ctxt evals eval_ts) fun pretty_failures ctxt target failures = diff -r 69e7fe18b7db -r fe31c7e7ebf4 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 11 22:19:09 2015 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 11 23:55:04 2015 +0200 @@ -330,13 +330,13 @@ fun print_wf (x, (gfp, wf)) = pprint_nt (fn () => Pretty.blk (0, - Pretty.text ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"") - @ Syntax.pretty_term ctxt (Const x) :: + Pretty.text ("The " ^ (if gfp then "co" else "") ^ "inductive predicate") @ + [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt (Const x)), Pretty.brk 1] @ Pretty.text (if wf then - "\" was proved well-founded. Nitpick can compute it \ + "was proved well-founded. Nitpick can compute it \ \efficiently." else - "\" could not be proved well-founded. Nitpick might need to \ + "could not be proved well-founded. Nitpick might need to \ \unroll it."))) val _ = if verbose then List.app print_wf (!wf_cache) else () val das_wort_formula = if falsify then "Negated conjecture" else "Formula" @@ -367,9 +367,9 @@ fun monotonicity_message Ts extra = let val pretties = map (pretty_maybe_quote keywords o pretty_for_type ctxt) Ts in Pretty.blk (0, - Pretty.text ("The type" ^ plural_s_for_list pretties ^ " ") @ - pretty_serial_commas "and" pretties @ - Pretty.text (" " ^ + Pretty.text ("The type" ^ plural_s_for_list pretties) @ [Pretty.brk 1] @ + pretty_serial_commas "and" pretties @ [Pretty.brk 1] @ + Pretty.text ( (if none_true monos then "passed the monotonicity test" else @@ -664,7 +664,7 @@ else " quasi genuine ") ^ das_wort_model) @ (case pretties_for_scope scope verbose of [] => [] - | pretties => Pretty.text " for " @ pretties) @ + | pretties => [Pretty.brk 1, Pretty.str "for", Pretty.brk 1] @ pretties) @ [Pretty.str ":", Pretty.fbrk])), Pretty.indent indent_size reconstructed_model]); print_t (K "% SZS output end FiniteModel");