--- a/src/HOL/Library/code_lazy.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/HOL/Library/code_lazy.ML Sat Apr 26 21:33:48 2025 +0200
@@ -629,7 +629,7 @@
fun cmp ((name1, _), (name2, _)) = string_ord (name1, name2)
val infos = Laziness_Data.get thy |> Symtab.dest |> map (apfst Long_Name.base_name) |> sort cmp
in
- Pretty.writeln_chunks (map (print_lazy_type thy) infos)
+ Pretty.writeln (Pretty.chunks (map (print_lazy_type thy) infos))
end;
--- a/src/HOL/Library/conditional_parametricity.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/HOL/Library/conditional_parametricity.ML Sat Apr 26 21:33:48 2025 +0200
@@ -110,7 +110,7 @@
(* Tactics *)
(* helper tactics for printing *)
fun error_tac ctxt msg st =
- (error (msg ^ "\n" ^ Goal_Display.string_of_goal ctxt st); Seq.single st);
+ (error (Goal_Display.print_goal ctxt msg st); Seq.single st);
fun error_tac' ctxt msg = SELECT_GOAL (error_tac ctxt msg);
--- a/src/HOL/SPARK/Tools/spark_commands.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Sat Apr 26 21:33:48 2025 +0200
@@ -88,7 +88,7 @@
Pretty.big_list (name ^ " " ^ f status)
(Element.pretty_ctxt ctxt context' @
Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |>
- Pretty.writeln_chunks2
+ Pretty.chunks2 |> Pretty.writeln
end;
val _ =
--- a/src/HOL/Tools/Function/lexicographic_order.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Sat Apr 26 21:33:48 2025 +0200
@@ -124,16 +124,12 @@
fun pr_unprovable_cell _ ((i,j), Less _) = []
| pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
- ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
- Goal_Display.string_of_goal ctxt st]
+ [Goal_Display.print_goal ctxt ("(" ^ row_index i ^ ", " ^ col_index j ^ ", <):") st]
| pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
- ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
- Goal_Display.string_of_goal ctxt st_less ^
- "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^
- Goal_Display.string_of_goal ctxt st_leq]
+ [Goal_Display.print_goal ctxt ("(" ^ row_index i ^ ", " ^ col_index j ^ ", <):") st_less ^ "\n" ^
+ Goal_Display.print_goal ctxt ("(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):") st_leq]
| pr_unprovable_cell ctxt ((i,j), False st) =
- ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
- Goal_Display.string_of_goal ctxt st]
+ [Goal_Display.print_goal ctxt ("(" ^ row_index i ^ ", " ^ col_index j ^ ", <):") st]
fun pr_unprovable_subgoals ctxt table =
table
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Sat Apr 26 21:33:48 2025 +0200
@@ -114,7 +114,7 @@
[Pretty.str (msg ^ ":"), Pretty.str ""] @
map (pretty_thm ctxt) with_superfluous_assumptions @
[Pretty.str "", Pretty.str end_msg]
- end |> Pretty.writeln_chunks
+ end |> Pretty.chunks |> Pretty.writeln
end
--- a/src/HOL/Tools/inductive.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/HOL/Tools/inductive.ML Sat Apr 26 21:33:48 2025 +0200
@@ -241,7 +241,7 @@
map (Pretty.mark_str o #1)
(Name_Space.markup_entries verbose ctxt space consts))),
Pretty.big_list "monotonicity rules:" (map (Thm.pretty_thm_item ctxt) monos)]
- end |> Pretty.writeln_chunks;
+ end |> Pretty.chunks |> Pretty.writeln;
(* inductive info *)
--- a/src/Provers/classical.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Provers/classical.ML Sat Apr 26 21:33:48 2025 +0200
@@ -643,7 +643,7 @@
Pretty.big_list "elimination rules (elim):" (pretty_thms unsafeEs),
Pretty.strs ("safe wrappers:" :: map #1 swrappers),
Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
- |> Pretty.writeln_chunks
+ |> Pretty.chunks |> Pretty.writeln
end;
--- a/src/Pure/General/output.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/General/output.ML Sat Apr 26 21:33:48 2025 +0200
@@ -25,7 +25,7 @@
val writelns: string list -> unit
val writelns_urgent: string list -> unit
val writeln_urgent: string -> unit
- val state: string -> unit
+ val state: string list-> unit
val information: string -> unit
val error_message': serial * string -> unit
val error_message: string -> unit
@@ -117,7 +117,7 @@
fun writeln s = writelns [s];
fun writelns_urgent ss = ! writeln_urgent_fn ss;
fun writeln_urgent s = writelns_urgent [s];
-fun state s = ! state_fn [s];
+fun state ss = ! state_fn ss;
fun information s = ! information_fn [s];
fun tracing s = ! tracing_fn [s];
fun warning s = ! warning_fn [s];
--- a/src/Pure/General/pretty.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/General/pretty.ML Sat Apr 26 21:33:48 2025 +0200
@@ -95,8 +95,6 @@
val chunks: T list -> T
val chunks2: T list -> T
val block_enclose: T * T -> T list -> T
- val writeln_chunks: T list -> unit
- val writeln_chunks2: T list -> unit
end;
structure Pretty: PRETTY =
@@ -239,6 +237,17 @@
(** formatting **)
+(* robust string output, with potential data loss *)
+
+fun robust_string_of out prt =
+ let
+ val bs = out prt;
+ val bs' =
+ if Bytes.size bs <= String.maxSize then bs
+ else out (from_ML (ML_Pretty.no_markup (to_ML prt)));
+ in Bytes.content bs' end;
+
+
(* output operations *)
type output_ops =
@@ -503,7 +512,7 @@
| output (Str (s, _)) = Bytes.add s;
in Bytes.build o output o output_tree ops false end;
-val symbolic_string_of = Bytes.content o symbolic_output;
+val symbolic_string_of = robust_string_of symbolic_output;
(* unformatted output: other markup only *)
@@ -518,14 +527,14 @@
in Bytes.build o output o output_tree ops false end;
fun unformatted_string_of prt =
- Bytes.content (unformatted (output_ops NONE) prt);
+ robust_string_of (unformatted (output_ops NONE)) prt;
(* output interfaces *)
fun output ops = if #symbolic ops then symbolic_output else format_tree ops;
-fun string_of_ops ops = Bytes.content o output ops;
+fun string_of_ops ops = robust_string_of (output ops);
fun string_of prt = string_of_ops (output_ops NONE) prt;
fun strings_of prt = Bytes.contents (output (output_ops NONE) prt);
@@ -553,19 +562,6 @@
fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
-fun string_of_text_fold prt = string_of prt |> Markup.markup Markup.text_fold;
-
-fun writeln_chunks prts =
- Output.writelns (Library.separate "\n" (map string_of_text_fold prts));
-
-fun writeln_chunks2 prts =
- (case try split_last prts of
- NONE => ()
- | SOME (prefix, last) =>
- (map (fn prt => Markup.markup Markup.text_fold (string_of prt ^ "\n") ^ "\n") prefix @
- [string_of_text_fold last])
- |> Output.writelns);
-
end;
--- a/src/Pure/Isar/attrib.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Isar/attrib.ML Sat Apr 26 21:33:48 2025 +0200
@@ -114,7 +114,7 @@
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
in
[Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table verbose ctxt attribs))]
- |> Pretty.writeln_chunks
+ |> Pretty.chunks |> Pretty.writeln
end;
val attribute_space = Name_Space.space_of_table o Attributes.get;
--- a/src/Pure/Isar/bundle.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Isar/bundle.ML Sat Apr 26 21:33:48 2025 +0200
@@ -110,8 +110,10 @@
end;
fun print_bundles verbose ctxt =
- Pretty.writeln_chunks
- (map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_all ctxt)));
+ Name_Space.markup_table verbose ctxt (get_all ctxt)
+ |> map (pretty_bundle ctxt)
+ |> Pretty.chunks
+ |> Pretty.writeln;
--- a/src/Pure/Isar/calculation.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Isar/calculation.ML Sat Apr 26 21:33:48 2025 +0200
@@ -47,7 +47,7 @@
let val pretty_thm = Thm.pretty_thm_item ctxt in
[Pretty.big_list "transitivity rules:" (map pretty_thm (get_trans_rules ctxt)),
Pretty.big_list "symmetry rules:" (map pretty_thm (get_sym_rules ctxt))]
- end |> Pretty.writeln_chunks;
+ end |> Pretty.chunks |> Pretty.writeln;
(* access calculation *)
--- a/src/Pure/Isar/class.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Isar/class.ML Sat Apr 26 21:33:48 2025 +0200
@@ -210,7 +210,8 @@
Sorts.all_classes algebra
|> sort (Name_Space.extern_ord ctxt class_space)
|> map prt_entry
- |> Pretty.writeln_chunks2
+ |> Pretty.chunks2
+ |> Pretty.writeln
end;
--- a/src/Pure/Isar/code.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Isar/code.ML Sat Apr 26 21:33:48 2025 +0200
@@ -1111,8 +1111,9 @@
fun apply_functrans ctxt functrans =
let
- fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks)
- (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns);
+ fun trace_eqns s eqns =
+ Pretty.writeln (Pretty.chunks
+ (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns));
val tracing = if Config.get ctxt simp_trace then trace_eqns else (K o K) ();
in
tap (tracing "before function transformation")
@@ -1252,7 +1253,7 @@
|> filter (fn (_, No_Case) => false | _ => true)
|> sort (string_ord o apply2 fst);
in
- Pretty.writeln_chunks [
+ Pretty.writeln (Pretty.chunks [
Pretty.block (
Pretty.str "types:" :: Pretty.fbrk
:: (Pretty.fbreaks o map pretty_type_spec) types
@@ -1265,7 +1266,7 @@
Pretty.str "cases:" :: Pretty.fbrk
:: (Pretty.fbreaks o map pretty_case) cases
)
- ]
+ ])
end;
--- a/src/Pure/Isar/context_rules.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML Sat Apr 26 21:33:48 2025 +0200
@@ -122,7 +122,7 @@
(map_filter (fn (_, (k, th)) =>
if k = (i, b) then SOME (Thm.pretty_thm_item ctxt th) else NONE)
(sort (int_ord o apply2 fst) rules));
- in Pretty.writeln_chunks (map prt_kind rule_kinds) end;
+ in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
(* access data *)
--- a/src/Pure/Isar/method.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Isar/method.ML Sat Apr 26 21:33:48 2025 +0200
@@ -396,7 +396,7 @@
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
in
[Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table verbose ctxt meths))]
- |> Pretty.writeln_chunks
+ |> Pretty.chunks |> Pretty.writeln
end;
--- a/src/Pure/Isar/outer_syntax.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Sat Apr 26 21:33:48 2025 +0200
@@ -95,7 +95,8 @@
dest_commands thy
|> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
|> map pretty_command
- |> Pretty.writeln_chunks;
+ |> Pretty.chunks
+ |> Pretty.writeln;
fun print_commands thy =
let
@@ -105,7 +106,8 @@
in
[Pretty.strs ("keywords:" :: map quote minor),
Pretty.big_list "commands:" (map pretty_command commands)]
- |> Pretty.writeln_chunks
+ |> Pretty.chunks
+ |> Pretty.writeln
end;
--- a/src/Pure/Isar/proof.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Isar/proof.ML Sat Apr 26 21:33:48 2025 +0200
@@ -492,7 +492,8 @@
val _ =
Context.subthy_id (Thm.theory_id goal, Context.theory_id thy) orelse
error "Bad background theory of goal state";
- val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
+ val _ = Thm.no_prems goal orelse
+ error (Pretty.string_of (Proof_Display.pretty_goal ctxt goal));
fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal);
@@ -521,13 +522,16 @@
val finished_goal_error = "Failed to finish proof";
+fun finished_goal_error_pos pos =
+ Pretty.block0 (Pretty.str finished_goal_error :: Pretty.here pos @ [Pretty.str ":"]);
+
fun finished_goal pos state =
let val (ctxt, {goal, ...}) = find_goal state in
if Thm.no_prems goal then Seq.Result state
else
Seq.Error (fn () =>
- finished_goal_error ^ Position.here pos ^ ":\n" ^
- Proof_Display.string_of_goal ctxt goal)
+ Pretty.string_of (Pretty.chunks
+ [finished_goal_error_pos pos, Proof_Display.pretty_goal ctxt goal]))
end;
--- a/src/Pure/Isar/proof_context.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Isar/proof_context.ML Sat Apr 26 21:33:48 2025 +0200
@@ -1563,7 +1563,7 @@
else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
end;
-fun print_abbrevs verbose = Pretty.writeln_chunks o pretty_abbrevs verbose true;
+fun print_abbrevs verbose = Pretty.writeln o Pretty.chunks o pretty_abbrevs verbose true;
(* term bindings *)
@@ -1595,7 +1595,7 @@
end;
fun print_local_facts verbose ctxt =
- Pretty.writeln_chunks (pretty_local_facts verbose ctxt);
+ Pretty.writeln (Pretty.chunks (pretty_local_facts verbose ctxt));
(* named local contexts *)
--- a/src/Pure/Isar/proof_display.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Isar/proof_display.ML Sat Apr 26 21:33:48 2025 +0200
@@ -12,7 +12,7 @@
val pretty_theorems: bool -> Proof.context -> Pretty.T list
val string_of_rule: Proof.context -> string -> thm -> string
val pretty_goal_header: thm -> Pretty.T
- val string_of_goal: Proof.context -> thm -> string
+ val pretty_goal: Proof.context -> thm -> Pretty.T
val pretty_goal_facts: Proof.context -> string -> thm list option -> Pretty.T list
val pretty_goal_inst: Proof.context -> term list list -> thm -> Pretty.T list
val method_error: string -> Position.T ->
@@ -200,10 +200,10 @@
fun pretty_goal_header goal =
Pretty.block ([Pretty.keyword1 "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
-end;
+fun pretty_goal ctxt goal =
+ Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal];
-fun string_of_goal ctxt goal =
- Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]);
+end;
(* goal facts *)
@@ -282,13 +282,14 @@
fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
let
val pr_header =
- "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
- "proof method" ^ Position.here pos ^ ":\n";
+ Pretty.block0
+ ([Pretty.str ("Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^ "proof method")]
+ @ Pretty.here pos @ [Pretty.str ":"]);
val pr_facts =
- if null facts then ""
- else Pretty.string_of (Pretty.chunks (pretty_goal_facts ctxt "using" (SOME facts))) ^ "\n";
- val pr_goal = string_of_goal ctxt goal;
- in pr_header ^ pr_facts ^ pr_goal end);
+ if null facts then []
+ else [Pretty.chunks (pretty_goal_facts ctxt "using" (SOME facts))];
+ val pr_goal = pretty_goal ctxt goal;
+ in Pretty.string_of (Pretty.chunks ([pr_header] @ pr_facts @ [pr_goal])) end);
(* results *)
--- a/src/Pure/Isar/toplevel.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Isar/toplevel.ML Sat Apr 26 21:33:48 2025 +0200
@@ -27,7 +27,6 @@
val presentation_state: Proof.context -> state
val pretty_context: state -> Pretty.T list
val pretty_state: state -> Pretty.T list
- val string_of_state: state -> string
val pretty_abstract: state -> Pretty.T
type presentation = state -> Latex.text
type transition
@@ -243,8 +242,6 @@
| Proof (prf, _) => Proof.pretty_state (Proof_Node.current prf)
| Skipped_Proof (d, _) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
-val string_of_state = pretty_state #> Pretty.chunks #> Pretty.string_of;
-
fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
val _ = ML_system_pp (fn _ => fn _ => Pretty.to_ML o pretty_abstract);
@@ -624,7 +621,7 @@
val enabled = is_none opt_err andalso Options.default_bool \<^system_option>\<open>show_states\<close>;
val opt_err' =
if enabled then
- (case Exn.capture (Output.state o string_of_state) st' of
+ (case Exn.capture (Output.state o Pretty.strings_of o Pretty.chunks o pretty_state) st' of
Exn.Exn exn => SOME exn
| Exn.Res _ => opt_err)
else opt_err;
--- a/src/Pure/ML/ml_pretty.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/ML/ml_pretty.ML Sat Apr 26 21:33:48 2025 +0200
@@ -9,9 +9,11 @@
datatype context = datatype PolyML.context
val markup_get: PolyML.context list -> string * string
val markup_context: string * string -> PolyML.context list
+ val no_markup_context: PolyML.context list -> PolyML.context list
val open_block_detect: PolyML.context list -> bool
val open_block_context: bool -> PolyML.context list
datatype pretty = datatype PolyML.pretty
+ val no_markup: pretty -> pretty
val block: pretty list -> pretty
val str: string -> pretty
val brk: FixedInt.int -> pretty
@@ -58,6 +60,9 @@
(if bg = "" then [] else [ContextProperty (markup_bg, bg)]) @
(if en = "" then [] else [ContextProperty (markup_en, en)]);
+val no_markup_context =
+ List.filter (fn ContextProperty (a, _) => a <> markup_bg andalso a <> markup_en | _ => true);
+
(* open_block flag *)
@@ -77,6 +82,9 @@
datatype pretty = datatype PolyML.pretty;
+fun no_markup (PrettyBlock (a, b, c, d)) = PrettyBlock (a, b, no_markup_context c, map no_markup d)
+ | no_markup a = a;
+
fun block prts = PrettyBlock (2, false, [], prts);
val str = PrettyString;
fun brk width = PrettyBreak (width, 0);
--- a/src/Pure/PIDE/command.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/PIDE/command.ML Sat Apr 26 21:33:48 2025 +0200
@@ -482,6 +482,7 @@
then
SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
print_fn = fn _ => fn st =>
- if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st)
+ if Toplevel.is_proof st
+ then Output.state (Pretty.strings_of (Pretty.chunks (Toplevel.pretty_state st)))
else ()}
else NONE);
--- a/src/Pure/Pure.thy Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Pure.thy Sat Apr 26 21:33:48 2025 +0200
@@ -1155,7 +1155,7 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_context\<close>
"print context of local theory target"
- (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
+ (Scan.succeed (Toplevel.keep (Pretty.writeln o Pretty.chunks o Toplevel.pretty_context)));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_theory\<close>
@@ -1275,7 +1275,7 @@
"print term bindings of proof context"
(Scan.succeed
(Toplevel.keep
- (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
+ (Pretty.writeln o Pretty.chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_facts\<close> "print facts of proof context"
@@ -1285,7 +1285,8 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_cases\<close> "print cases of proof context"
(Scan.succeed
- (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
+ (Toplevel.keep
+ (Pretty.writeln o Pretty.chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>print_statement\<close>
@@ -1340,7 +1341,9 @@
Outer_Syntax.command \<^command_keyword>\<open>print_state\<close>
"print current proof state (if present)"
(opt_modes >> (fn modes =>
- Toplevel.keep (Print_Mode.with_modes modes (Output.writeln o Toplevel.string_of_state))));
+ Toplevel.keep
+ (Print_Mode.with_modes modes
+ (Output.writelns o Pretty.strings_of o Pretty.chunks o Toplevel.pretty_state))));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>welcome\<close> "print welcome message"
@@ -1411,7 +1414,7 @@
NONE => (Theory.parents_of thy, [thy])
| SOME (xs, NONE) => (map check xs, [thy])
| SOME (xs, SOME ys) => (map check xs, map check ys))
- |> map pretty_thm |> Pretty.writeln_chunks
+ |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
end)));
in end\<close>
--- a/src/Pure/Syntax/syntax.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Syntax/syntax.ML Sat Apr 26 21:33:48 2025 +0200
@@ -714,9 +714,9 @@
in
-fun print_gram syn = Pretty.writeln_chunks (pretty_gram syn);
-fun print_trans syn = Pretty.writeln_chunks (pretty_trans syn);
-fun print_syntax syn = Pretty.writeln_chunks (pretty_gram syn @ pretty_trans syn);
+fun print_gram syn = Pretty.writeln (Pretty.chunks (pretty_gram syn));
+fun print_trans syn = Pretty.writeln (Pretty.chunks (pretty_trans syn));
+fun print_syntax syn = Pretty.writeln (Pretty.chunks (pretty_gram syn @ pretty_trans syn));
end;
--- a/src/Pure/Syntax/syntax_phases.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Sat Apr 26 21:33:48 2025 +0200
@@ -927,7 +927,7 @@
pretty_checks "term_checks" term_checks @
pretty_checks "typ_unchecks" typ_unchecks @
pretty_checks "term_unchecks" term_unchecks
- end |> Pretty.writeln_chunks;
+ end |> Pretty.chunks |> Pretty.writeln;
local
--- a/src/Pure/Thy/document_antiquotation.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML Sat Apr 26 21:33:48 2025 +0200
@@ -116,7 +116,7 @@
in
[Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
- end |> Pretty.writeln_chunks;
+ end |> Pretty.chunks |> Pretty.writeln;
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt));
fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
--- a/src/Pure/goal.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/goal.ML Sat Apr 26 21:33:48 2025 +0200
@@ -80,7 +80,7 @@
*)
fun check_finished ctxt th =
if Thm.no_prems th then th
- else raise THM ("Proof failed.\n" ^ Goal_Display.string_of_goal ctxt th, 0, [th]);
+ else raise THM (Goal_Display.print_goal ctxt "Proof failed." th, 0, [th]);
fun finish ctxt = check_finished ctxt #> conclude;
--- a/src/Pure/goal_display.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/goal_display.ML Sat Apr 26 21:33:48 2025 +0200
@@ -11,7 +11,7 @@
val show_main_goal: bool Config.T
val pretty_goals: Proof.context -> thm -> Pretty.T list
val pretty_goal: Proof.context -> thm -> Pretty.T
- val string_of_goal: Proof.context -> thm -> string
+ val print_goal: Proof.context -> string -> thm -> string
end;
structure Goal_Display: GOAL_DISPLAY =
@@ -117,7 +117,10 @@
end;
val pretty_goal = Pretty.chunks oo pretty_goals;
-val string_of_goal = Pretty.string_of oo pretty_goal;
+
+fun print_goal ctxt header state =
+ (Pretty.string_of o Pretty.chunks)
+ ((if header = "" then [] else [Pretty.str header]) @ pretty_goals ctxt state);
end;
--- a/src/Pure/tactical.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Pure/tactical.ML Sat Apr 26 21:33:48 2025 +0200
@@ -176,7 +176,7 @@
(*Print the current proof state and pass it on.*)
fun print_tac ctxt msg st =
- (tracing (msg ^ "\n" ^ Goal_Display.string_of_goal ctxt st); Seq.single st);
+ (tracing (Goal_Display.print_goal ctxt msg st); Seq.single st);
(*Deterministic REPEAT: only retains the first outcome;
--- a/src/Tools/Code/code_preproc.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Tools/Code/code_preproc.ML Sat Apr 26 21:33:48 2025 +0200
@@ -262,7 +262,7 @@
val post = (#post o the_thmproc) thy;
val functrans = (map fst o #functrans o the_thmproc) thy;
in
- Pretty.writeln_chunks [
+ Pretty.writeln (Pretty.chunks [
Pretty.block [
Pretty.str "preprocessing simpset:",
Pretty.fbrk,
@@ -278,7 +278,7 @@
:: Pretty.fbrk
:: (Pretty.fbreaks o map Pretty.str) functrans
)
- ]
+ ])
end;
fun simple_functrans f ctxt eqns = case f ctxt (map fst eqns)
--- a/src/Tools/induct.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Tools/induct.ML Sat Apr 26 21:33:48 2025 +0200
@@ -259,7 +259,7 @@
pretty_rules ctxt "induct pred:" inductP,
pretty_rules ctxt "cases type:" casesT,
pretty_rules ctxt "cases pred:" casesP]
- |> Pretty.writeln_chunks
+ |> Pretty.chunks |> Pretty.writeln
end;
val _ =
--- a/src/Tools/subtyping.ML Sat Apr 26 08:34:03 2025 +0200
+++ b/src/Tools/subtyping.ML Sat Apr 26 21:33:48 2025 +0200
@@ -1086,7 +1086,7 @@
[Pretty.big_list "coercions between base types:" (map show_coercion simple),
Pretty.big_list "other coercions:" (map show_coercion complex),
Pretty.big_list "coercion maps:" (map show_map tmaps)]
- end |> Pretty.writeln_chunks;
+ end |> Pretty.chunks |> Pretty.writeln;
(* attribute setup *)