# HG changeset patch # User wenzelm # Date 1718021139 -7200 # Node ID 559909bd7715a5273ad8b97cf4de9dc24302ed68 # Parent e4e643705d90cfbed730d60a364af945adef44b3 clarified signature: more operations; diff -r e4e643705d90 -r 559909bd7715 src/HOL/Library/code_test.ML --- 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 *) diff -r e4e643705d90 -r 559909bd7715 src/HOL/SPARK/Tools/spark_vcs.ML --- 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); diff -r e4e643705d90 -r 559909bd7715 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r e4e643705d90 -r 559909bd7715 src/Pure/General/pretty.ML --- 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]; diff -r e4e643705d90 -r 559909bd7715 src/Pure/Isar/proof_context.ML --- 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) => diff -r e4e643705d90 -r 559909bd7715 src/Pure/Isar/proof_display.ML --- 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 = diff -r e4e643705d90 -r 559909bd7715 src/Pure/Tools/find_theorems.ML --- 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; diff -r e4e643705d90 -r 559909bd7715 src/Pure/unify.ML --- 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 " \\<^sup>?", Pretty.brk 1, termT t]); - in Pretty.string_of prt end; + in Pretty.string_of (Pretty.block0 [termT u, Pretty.str " \\<^sup>?", Pretty.brk 1, termT t]) end; in cond_tracing context (fn () => msg); List.app (fn dp => cond_tracing context (fn () => pdp dp)) dpairs diff -r e4e643705d90 -r 559909bd7715 src/Tools/Code/code_target.ML --- 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;