# HG changeset patch # User wenzelm # Date 1718054673 -7200 # Node ID 4bed658a01fc8eb273168c418551d67faa56ee9a # Parent a6d5de03ffeb0118b9d64a4ffdbccb8d72d0252d# Parent 6f25a035069c6f71a945c381ddf1d9facfcf4272 merged diff -r a6d5de03ffeb -r 4bed658a01fc src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML Mon Jun 10 21:32:24 2024 +0200 +++ b/src/HOL/Library/code_test.ML Mon Jun 10 23:24:33 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 a6d5de03ffeb -r 4bed658a01fc src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Mon Jun 10 21:32:24 2024 +0200 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Mon Jun 10 23:24:33 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 a6d5de03ffeb -r 4bed658a01fc src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Jun 10 21:32:24 2024 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Jun 10 23:24:33 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 a6d5de03ffeb -r 4bed658a01fc src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jun 10 21:32:24 2024 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Mon Jun 10 23:24:33 2024 +0200 @@ -223,7 +223,7 @@ fun is_that_fact th = exists_subterm (fn Free (s, _) => s = skolem_thesis | _ => false) (Thm.prop_of th) - andalso String.isSuffix sep_that (Thm_Name.short (Thm.get_name_hint th)) + andalso String.isSuffix sep_that (#1 (Thm.get_name_hint th)) datatype interest = Deal_Breaker | Interesting | Boring diff -r a6d5de03ffeb -r 4bed658a01fc src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Jun 10 21:32:24 2024 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Jun 10 23:24:33 2024 +0200 @@ -94,7 +94,7 @@ val assms = Pretty.enum " and " "using " " shows " (map (Thm.pretty_thm ctxt) assms) val concl = Syntax.pretty_term ctxt concl in - tracing (Pretty.string_of (Pretty.blk (2, Pretty.breaks [time, assms, concl]))) + tracing (Pretty.string_of (Pretty.block (Pretty.breaks [time, assms, concl]))) end fun take_time timeout tac arg = diff -r a6d5de03ffeb -r 4bed658a01fc src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Mon Jun 10 21:32:24 2024 +0200 +++ b/src/Pure/General/pretty.ML Mon Jun 10 23:24:33 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 a6d5de03ffeb -r 4bed658a01fc src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Mon Jun 10 21:32:24 2024 +0200 +++ b/src/Pure/Isar/proof_context.ML Mon Jun 10 23:24:33 2024 +0200 @@ -414,14 +414,15 @@ then local_facts else global_facts end; -fun markup_extern_fact ctxt name = - let - val facts = facts_of_fact ctxt name; - val (markup, xname) = Facts.markup_extern ctxt facts name; - val markups = - if Facts.is_dynamic facts name then [markup, Markup.dynamic_fact name] - else [markup]; - in (markups, xname) end; +fun markup_extern_fact _ "" = ([], "") + | markup_extern_fact ctxt name = + let + val facts = facts_of_fact ctxt name; + val (markup, xname) = Facts.markup_extern ctxt facts name; + val markups = + if Facts.is_dynamic facts name then [markup, Markup.dynamic_fact name] + else [markup]; + in (markups, xname) end; fun pretty_thm_name ctxt (name, i) = Facts.pretty_thm_name (Context.Proof ctxt) (facts_of_fact ctxt name) (name, i); @@ -442,8 +443,7 @@ fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt); -fun pretty_fact_name ctxt a = - Pretty.block [Pretty.marks_str (markup_extern_fact ctxt a), Pretty.str ":"]; +fun pretty_fact_name ctxt a = Pretty.marks_str (markup_extern_fact ctxt a); fun pretty_fact ctxt = let @@ -451,9 +451,11 @@ val pretty_thms = map (Thm.pretty_thm_item ctxt); in fn ("", [th]) => pretty_thm th - | ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths)) - | (a, [th]) => Pretty.block [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm th] - | (a, ths) => Pretty.block (Pretty.fbreaks (pretty_fact_name ctxt a :: 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) => + Pretty.block (Pretty.fbreaks (pretty_fact_name ctxt a :: Pretty.str ":" :: pretty_thms ths)) end; diff -r a6d5de03ffeb -r 4bed658a01fc src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Mon Jun 10 21:32:24 2024 +0200 +++ b/src/Pure/Isar/proof_display.ML Mon Jun 10 23:24:33 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 a6d5de03ffeb -r 4bed658a01fc src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Mon Jun 10 21:32:24 2024 +0200 +++ b/src/Pure/Tools/find_theorems.ML Mon Jun 10 23:24:33 2024 +0200 @@ -17,11 +17,12 @@ } val query_parser: (bool * string criterion) list parser val read_query: Position.T -> string -> (bool * string criterion) list + val all_facts_of: Proof.context -> (Thm_Name.T * thm) list val find_theorems: Proof.context -> thm option -> int option -> bool -> - (bool * term criterion) list -> int option * (Facts.ref * thm) list + (bool * term criterion) list -> int option * (Thm_Name.T * thm) list val find_theorems_cmd: Proof.context -> thm option -> int option -> bool -> - (bool * string criterion) list -> int option * (Facts.ref * thm) list - val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T + (bool * string criterion) list -> int option * (Thm_Name.T * thm) list + val pretty_thm: Proof.context -> Thm_Name.T * thm -> Pretty.T val pretty_theorems: Proof.state -> int option -> bool -> (bool * string criterion) list -> Pretty.T val proof_state: Toplevel.state -> Proof.state @@ -77,7 +78,7 @@ (** search criterion filters **) (*generated filters are to be of the form - input: (Facts.ref * thm) + input: (Thm_Name.T * thm) output: (p:int, s:int, t:int) option, where NONE indicates no match p is the primary sorting criterion @@ -124,8 +125,8 @@ (* filter_name *) -fun filter_name str_pat (thmref, _) = - if match_string str_pat (Facts.ref_name thmref) +fun filter_name str_pat (thm_name: Thm_Name.T, _) = + if match_string str_pat (#1 thm_name) then SOME (0, 0, 0) else NONE; @@ -333,7 +334,6 @@ local -val index_ord = option_ord (K EQUAL); val hidden_ord = bool_ord o apply2 Long_Name.is_hidden; val qual_ord = int_ord o apply2 Long_Name.count; val txt_ord = int_ord o apply2 size; @@ -341,7 +341,7 @@ fun nicer_name ((a, x), i) ((b, y), j) = (case bool_ord (a, b) of EQUAL => (case hidden_ord (x, y) of EQUAL => - (case index_ord (i, j) of EQUAL => + (case int_ord (i, j) of EQUAL => (case qual_ord (x, y) of EQUAL => txt_ord (x, y) | ord => ord) | ord => ord) | ord => ord) @@ -366,13 +366,7 @@ val facts = Proof_Context.facts_of_fact ctxt name; val space = Facts.space_of facts; in (Facts.is_dynamic facts name, Name_Space.extern_shortest ctxt space name) end; - - fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) = - nicer_name (extern_shortest x, i) (extern_shortest y, j) - | nicer (Facts.Fact _) (Facts.Named _) = true - | nicer (Facts.Named _) (Facts.Fact _) = false - | nicer (Facts.Fact _) (Facts.Fact _) = true; - in nicer end; + in fn (x, i) => fn (y, j) => nicer_name (extern_shortest x, i) (extern_shortest y, j) end; fun rem_thm_dups nicer xs = (xs ~~ (1 upto length xs)) @@ -398,7 +392,7 @@ in (Facts.dest_all (Context.Proof ctxt) false [global_facts] local_facts @ Facts.dest_all (Context.Proof ctxt) false [] global_facts) - |> maps Facts.selections + |> maps Thm_Name.make_list |> map (apsnd transfer) end; @@ -459,21 +453,14 @@ local -fun pretty_ref ctxt thmref = - let - val (name, sel) = - (case thmref of - Facts.Named ((name, _), sel) => (name, sel) - | Facts.Fact _ => raise Fail "Illegal literal fact"); - in - [Pretty.marks_str (#1 (Proof_Context.markup_extern_fact ctxt name), name), - Pretty.str (Facts.string_of_selection sel), Pretty.str ":", Pretty.brk 1] - end; +fun pretty_thm_head ctxt (name, i) = + [Pretty.marks_str (#1 (Proof_Context.markup_extern_fact ctxt name), name), + Pretty.str (Thm_Name.print_suffix (name, i)), Pretty.str ":", Pretty.brk 1]; in -fun pretty_thm ctxt (thmref, thm) = - Pretty.block (pretty_ref ctxt thmref @ [Thm.pretty_thm ctxt thm]); +fun pretty_thm ctxt (thm_name, thm) = + Pretty.block (pretty_thm_head ctxt thm_name @ [Thm.pretty_thm ctxt thm]); fun pretty_theorems state opt_limit rem_dups raw_criteria = let @@ -505,7 +492,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 a6d5de03ffeb -r 4bed658a01fc src/Pure/thm_name.ML --- a/src/Pure/thm_name.ML Mon Jun 10 21:32:24 2024 +0200 +++ b/src/Pure/thm_name.ML Mon Jun 10 23:24:33 2024 +0200 @@ -15,6 +15,7 @@ structure Table: TABLE val empty: T val is_empty: T -> bool + val make_list: string * 'a list -> (T * 'a) list type P = T * Position.T val none: P @@ -44,6 +45,9 @@ val empty: T = ("", 0); fun is_empty ((a, _): T) = a = ""; +fun make_list (a, [b]) = [((a, 0): T, b)] + | make_list (a, bs) = map_index (fn (i, b) => ((a, i + 1), b)) bs; + (* type P *) diff -r a6d5de03ffeb -r 4bed658a01fc src/Pure/unify.ML --- a/src/Pure/unify.ML Mon Jun 10 21:32:24 2024 +0200 +++ b/src/Pure/unify.ML Mon Jun 10 23:24:33 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 a6d5de03ffeb -r 4bed658a01fc src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Mon Jun 10 21:32:24 2024 +0200 +++ b/src/Tools/Code/code_target.ML Mon Jun 10 23:24:33 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;