# HG changeset patch # User wenzelm # Date 1745523580 -7200 # Node ID bcee022fbe3063d8338e633def89647b156a8b2a # Parent 0133fe6a1f55ecb66c0f47fdbde81e00e8fd6ff8 more scalable; diff -r 0133fe6a1f55 -r bcee022fbe30 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Thu Apr 24 20:42:04 2025 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Thu Apr 24 21:39:40 2025 +0200 @@ -244,55 +244,53 @@ local -fun string_of_stmts ctxt args = +fun pretty_stmts ctxt args = Attrib.eval_thms ctxt args |> map (Element.pretty_statement ctxt Thm.theoremK) - |> Pretty.chunks2 |> Pretty.string_of; + |> Pretty.chunks2; -fun string_of_thms ctxt args = - Pretty.string_of (Proof_Context.pretty_fact ctxt ("", Attrib.eval_thms ctxt args)); +fun pretty_thms ctxt args = + Proof_Context.pretty_fact ctxt ("", Attrib.eval_thms ctxt args); -fun string_of_prfs full state arg = - Pretty.string_of - (case arg of - NONE => - let - val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state); - val thy = Proof_Context.theory_of ctxt; - val prf = Thm.proof_of thm; - val prop = Thm.full_prop_of thm; - val prf' = Proofterm.rewrite_proof_notypes ([], []) prf; - in - Proof_Syntax.pretty_proof ctxt - (if full then Proofterm.reconstruct_proof thy prop prf' else prf') - end - | SOME srcs => - let - val ctxt = Toplevel.context_of state; - val pretty_proof = Proof_Syntax.pretty_standard_proof_of ctxt full; - in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end); +fun pretty_prfs full state arg = + (case arg of + NONE => + let + val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state); + val thy = Proof_Context.theory_of ctxt; + val prf = Thm.proof_of thm; + val prop = Thm.full_prop_of thm; + val prf' = Proofterm.rewrite_proof_notypes ([], []) prf; + in + Proof_Syntax.pretty_proof ctxt + (if full then Proofterm.reconstruct_proof thy prop prf' else prf') + end + | SOME srcs => + let + val ctxt = Toplevel.context_of state; + val pretty_proof = Proof_Syntax.pretty_standard_proof_of ctxt full; + in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end); -fun string_of_prop ctxt s = +fun pretty_prop ctxt s = let val prop = Syntax.read_prop ctxt s; val ctxt' = Proof_Context.augment prop ctxt; - in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end; + in Pretty.quote (Syntax.pretty_term ctxt' prop) end; -fun string_of_term ctxt s = +fun pretty_term ctxt s = let val t = Syntax.read_term ctxt s; val T = Term.type_of t; val ctxt' = Proof_Context.augment t ctxt; in - Pretty.string_of - (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk, - Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)]) + Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk, + Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)] end; -fun string_of_type ctxt (s, NONE) = +fun pretty_type ctxt (s, NONE) = let val T = Syntax.read_typ ctxt s - in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end - | string_of_type ctxt (s1, SOME s2) = + in Pretty.quote (Syntax.pretty_typ ctxt T) end + | pretty_type ctxt (s1, SOME s2) = let val ctxt' = Config.put show_sorts true ctxt; val raw_T = Syntax.parse_typ ctxt' s1; @@ -301,19 +299,19 @@ Syntax.check_term ctxt' (Logic.mk_type raw_T |> Type.constraint (Term.itselfT (Type_Infer.anyT S))) |> Logic.dest_type; - in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt' T)) end; + in Pretty.quote (Syntax.pretty_typ ctxt' T) end; -fun print_item string_of (modes, arg) = Toplevel.keep (fn state => - Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ()); +fun print_item pretty (modes, arg) = Toplevel.keep (fn state => + Print_Mode.with_modes modes (fn () => Pretty.writeln (pretty state arg)) ()); in -val print_stmts = print_item (string_of_stmts o Toplevel.context_of); -val print_thms = print_item (string_of_thms o Toplevel.context_of); -val print_prfs = print_item o string_of_prfs; -val print_prop = print_item (string_of_prop o Toplevel.context_of); -val print_term = print_item (string_of_term o Toplevel.context_of); -val print_type = print_item (string_of_type o Toplevel.context_of); +val print_stmts = print_item (pretty_stmts o Toplevel.context_of); +val print_thms = print_item (pretty_thms o Toplevel.context_of); +val print_prfs = print_item o pretty_prfs; +val print_prop = print_item (pretty_prop o Toplevel.context_of); +val print_term = print_item (pretty_term o Toplevel.context_of); +val print_type = print_item (pretty_type o Toplevel.context_of); end;