--- 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 *)
--- 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);
--- 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
--- 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
--- 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 =
--- 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];
--- 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;
--- 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 =
--- 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;
--- 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 *)
--- 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 " \<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 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;