--- a/src/HOL/Library/code_test.ML Mon Jun 10 14:04:52 2024 +0200
+++ b/src/HOL/Library/code_test.ML Mon Jun 10 14:05:39 2024 +0200
@@ -131,7 +131,7 @@
pretty_eval ctxt evals eval_ts)
fun pretty_failures ctxt target failures =
- Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
+ Pretty.block0 (Pretty.fbreaks (map (pretty_failure ctxt target) failures))
(* driver invocation *)
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Mon Jun 10 14:04:52 2024 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Mon Jun 10 14:05:39 2024 +0200
@@ -737,7 +737,7 @@
apsnd (cons (name, (trace, ps, cs))))
vcs ([], []);
-fun insert_break prt = Pretty.blk (0, [Pretty.fbrk, prt]);
+fun insert_break prt = Pretty.block0 [Pretty.fbrk, prt];
fun print_open_vcs f vcs =
(Pretty.writeln (f (pp_open_vcs (snd (partition_vcs vcs)))); vcs);
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Jun 10 14:04:52 2024 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Jun 10 14:05:39 2024 +0200
@@ -305,8 +305,8 @@
got_all_mono_user_axioms andalso no_poly_user_axioms
fun print_wf (x, (gfp, wf)) =
- pprint_nt (fn () => Pretty.blk (0,
- Pretty.text ("The " ^ (if gfp then "co" else "") ^ "inductive predicate") @
+ pprint_nt (fn () => Pretty.block0
+ (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 \
@@ -342,8 +342,8 @@
val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
fun monotonicity_message Ts extra =
let val pretties = map (pretty_maybe_quote ctxt o pretty_for_type ctxt) Ts in
- Pretty.blk (0,
- Pretty.text ("The type" ^ plural_s_for_list pretties) @ [Pretty.brk 1] @
+ Pretty.block0
+ (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
@@ -631,8 +631,8 @@
codatatypes_ok
in
(pprint_a (Pretty.chunks
- [Pretty.blk (0,
- (Pretty.text ((if mode = Auto_Try then "Auto " else "") ^
+ [Pretty.block0
+ ((Pretty.text ((if mode = Auto_Try then "Auto " else "") ^
"Nitpick found a" ^
(if not genuine then " potentially spurious "
else if genuine_means_genuine then " "
@@ -791,8 +791,8 @@
print_nt (K "The scope specification is inconsistent")
else if verbose then
pprint_nt (fn () => Pretty.chunks
- [Pretty.blk (0,
- Pretty.text ((if n > 1 then
+ [Pretty.block0
+ (Pretty.text ((if n > 1 then
"Batch " ^ string_of_int (j + 1) ^ " of " ^
signed_string_of_int n ^ ": "
else
--- a/src/Pure/General/pretty.ML Mon Jun 10 14:04:52 2024 +0200
+++ b/src/Pure/General/pretty.ML Mon Jun 10 14:05:39 2024 +0200
@@ -33,6 +33,8 @@
val breaks: T list -> T list
val fbreaks: T list -> T list
val blk: int * T list -> T
+ val block0: T list -> T
+ val block1: T list -> T
val block: T list -> T
val strs: string list -> T
val markup: Markup.T -> T list -> T
@@ -159,6 +161,8 @@
fun blk (indent, es) =
markup_block {markup = Markup.empty, consistent = false, indent = indent} es;
+fun block0 prts = blk (0, prts);
+fun block1 prts = blk (1, prts);
fun block prts = blk (2, prts);
val strs = block o breaks o map str;
@@ -177,8 +181,8 @@
val paragraph = markup Markup.paragraph;
val para = paragraph o text;
-fun quote prt = blk (1, [str "\"", prt, str "\""]);
-fun cartouche prt = blk (1, [str Symbol.open_, prt, str Symbol.close]);
+fun quote prt = block1 [str "\"", prt, str "\""];
+fun cartouche prt = block1 [str Symbol.open_, prt, str Symbol.close];
fun separate sep prts =
flat (Library.separate [str sep, brk 1] (map single prts));
@@ -208,7 +212,7 @@
fun big_list name prts = block (fbreaks (str name :: prts));
fun indent 0 prt = prt
- | indent n prt = blk (0, [str (Symbol.spaces n), prt]);
+ | indent n prt = block0 [str (Symbol.spaces n), prt];
fun unbreakable (Block (m, consistent, indent, es, len)) =
Block (m, consistent, indent, map unbreakable es, len)
@@ -373,9 +377,9 @@
fun chunks2 prts =
(case try split_last prts of
- NONE => blk (0, [])
+ NONE => block0 []
| SOME (prefix, last) =>
- blk (0, maps (fn prt => [text_fold [prt, fbrk], fbrk]) prefix @ [text_fold [last]]));
+ block0 (maps (fn prt => [text_fold [prt, fbrk], fbrk]) prefix @ [text_fold [last]]));
fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
--- a/src/Pure/Isar/proof_context.ML Mon Jun 10 14:04:52 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML Mon Jun 10 14:05:39 2024 +0200
@@ -450,7 +450,7 @@
val pretty_thms = map (Thm.pretty_thm_item ctxt);
in
fn ("", [th]) => pretty_thm th
- | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths))
+ | ("", ths) => Pretty.block0 (Pretty.fbreaks (pretty_thms ths))
| (a, [th]) =>
Pretty.block [pretty_fact_name ctxt a, Pretty.str ":", Pretty.brk 1, pretty_thm th]
| (a, ths) =>
--- a/src/Pure/Isar/proof_display.ML Mon Jun 10 14:04:52 2024 +0200
+++ b/src/Pure/Isar/proof_display.ML Mon Jun 10 14:05:39 2024 +0200
@@ -369,10 +369,10 @@
else
print
(case facts of
- [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
- Proof_Context.pretty_fact ctxt fact])
- | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
- Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]))
+ [fact] => Pretty.block1 [pretty_fact_name pos (kind, name), Pretty.fbrk,
+ Proof_Context.pretty_fact ctxt fact]
+ | _ => Pretty.block1 [pretty_fact_name pos (kind, name), Pretty.fbrk,
+ Pretty.block1 (Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])])
end;
fun print_theorem pos ctxt fact =
--- a/src/Pure/Tools/find_theorems.ML Mon Jun 10 14:04:52 2024 +0200
+++ b/src/Pure/Tools/find_theorems.ML Mon Jun 10 14:05:39 2024 +0200
@@ -505,7 +505,7 @@
else
Pretty.str (tally_msg ^ ":") ::
grouped 10 Par_List.map (Pretty.item o single o pretty_thm ctxt) (rev theorems))
- end |> Pretty.fbreaks |> curry Pretty.blk 0;
+ end |> Pretty.fbreaks |> Pretty.block0;
end;
--- a/src/Pure/unify.ML Mon Jun 10 14:04:52 2024 +0200
+++ b/src/Pure/unify.ML Mon Jun 10 14:05:39 2024 +0200
@@ -580,8 +580,7 @@
val ctxt = Context.proof_of context;
fun termT t =
Syntax.pretty_term ctxt (Envir.norm_term env (Logic.rlist_abs (rbinder, t)));
- val prt = Pretty.blk (0, [termT u, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, termT t]);
- in Pretty.string_of prt end;
+ in Pretty.string_of (Pretty.block0 [termT u, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, termT t]) end;
in
cond_tracing context (fn () => msg);
List.app (fn dp => cond_tracing context (fn () => pdp dp)) dpairs
--- a/src/Tools/Code/code_target.ML Mon Jun 10 14:04:52 2024 +0200
+++ b/src/Tools/Code/code_target.ML Mon Jun 10 14:05:39 2024 +0200
@@ -651,7 +651,7 @@
(arrange check_const_syntax) (arrange check_tyco_syntax)
(arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I))
(arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_syms) =>
- (Pretty.blk (0, Pretty.fbreaks (map Code_Printer.str (split_lines raw_content))),
+ (Pretty.block0 (Pretty.fbreaks (map Code_Printer.str (split_lines raw_content))),
map (prep_syms ctxt) raw_syms)))
end;