--- a/src/HOL/Tools/ATP/atp_util.ML Wed Mar 06 09:43:25 2024 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML Tue Feb 27 13:46:42 2024 +0100
@@ -6,6 +6,7 @@
signature ATP_UTIL =
sig
+ val proof_cartouches: bool Config.T
val timestamp : unit -> string
val hashw : word * word -> word
val hashw_string : string * word -> word
@@ -18,7 +19,7 @@
val find_enclosed : string -> string -> string -> string list
val nat_subscript : int -> string
val unquote_tvar : string -> string
- val maybe_quote : Keyword.keywords -> string -> string
+ val maybe_quote : Proof.context -> string -> string
val string_of_ext_time : bool * Time.time -> string
val string_of_time : Time.time -> string
val type_instance : theory -> typ -> typ -> bool
@@ -56,6 +57,8 @@
structure ATP_Util : ATP_UTIL =
struct
+val proof_cartouches = Attrib.setup_config_bool \<^binding>\<open>atp_proof_cartouches\<close> (K false)
+
fun forall2 _ [] [] = true
| forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
| forall2 _ _ _ = false
@@ -138,11 +141,15 @@
val unquery_var = perhaps (try (unprefix "?"))
val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode
-fun maybe_quote keywords y =
- let val s = YXML.content_of y in
+fun maybe_quote ctxt y =
+ let
+ val s = YXML.content_of y
+ val is_literal = (Keyword.is_literal o Thy_Header.get_keywords') ctxt
+ val gen_quote = if Config.get ctxt proof_cartouches then cartouche else quote
+ in
y |> ((not (is_long_identifier (unquote_tvar s)) andalso
not (is_long_identifier (unquery_var s))) orelse
- Keyword.is_literal keywords s) ? quote
+ is_literal s) ? gen_quote
end
fun string_of_ext_time (plus, time) =
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Mar 06 09:43:25 2024 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Feb 27 13:46:42 2024 +0100
@@ -202,7 +202,6 @@
val time_start = Time.now ()
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
- val keywords = Thy_Header.get_keywords thy
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
boxes, finitizes, monos, wfs, sat_solver, falsify, debug, verbose,
overlord, spy, user_axioms, assms, whacks, merge_type_vars,
@@ -342,7 +341,7 @@
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 keywords o pretty_for_type ctxt) Ts in
+ 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_serial_commas "and" pretties @ [Pretty.brk 1] @
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Mar 06 09:43:25 2024 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Feb 27 13:46:42 2024 +0100
@@ -181,8 +181,8 @@
fun standard_blocks s = map (Pretty.block o cons (Pretty.str (s ^ " ")))
val (primary_cards, secondary_cards, maxes, iters, miscs) =
quintuple_for_scope
- (fn ctxt => pretty_maybe_quote (Thy_Header.get_keywords' ctxt) o pretty_for_type ctxt)
- (fn ctxt => pretty_maybe_quote (Thy_Header.get_keywords' ctxt) o Syntax.pretty_term ctxt)
+ (fn ctxt => pretty_maybe_quote ctxt o pretty_for_type ctxt)
+ (fn ctxt => pretty_maybe_quote ctxt o Syntax.pretty_term ctxt)
Pretty.str scope
in
standard_blocks "card" primary_cards @
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Mar 06 09:43:25 2024 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Feb 27 13:46:42 2024 +0100
@@ -69,7 +69,7 @@
val eta_expand : typ list -> term -> int -> term
val DETERM_TIMEOUT : Time.time -> tactic -> tactic
val indent_size : int
- val pretty_maybe_quote : Keyword.keywords -> Pretty.T -> Pretty.T
+ val pretty_maybe_quote : Proof.context -> Pretty.T -> Pretty.T
val hash_term : term -> int
val spying : bool -> (unit -> Proof.state * int * string) -> unit
end;
@@ -279,9 +279,9 @@
val maybe_quote = ATP_Util.maybe_quote
-fun pretty_maybe_quote keywords pretty =
+fun pretty_maybe_quote ctxt pretty =
let val s = Pretty.unformatted_string_of pretty
- in if maybe_quote keywords s = s then pretty else Pretty.quote pretty end
+ in if maybe_quote ctxt s = s then pretty else Pretty.quote pretty end
val hashw = ATP_Util.hashw
val hashw_string = ATP_Util.hashw_string
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Wed Mar 06 09:43:25 2024 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Tue Feb 27 13:46:42 2024 +0100
@@ -373,7 +373,6 @@
fun string_of_isar_proof ctxt0 i n proof =
let
- val keywords = Thy_Header.get_keywords' ctxt0
(* Make sure only type constraints inserted by the type annotation code are printed. *)
val ctxt = ctxt0
@@ -408,7 +407,7 @@
|> annotate_types_in_term ctxt
|> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
|> simplify_spaces
- |> maybe_quote keywords),
+ |> maybe_quote ctxt),
ctxt |> perhaps (try (Proof_Context.augment term)))
fun using_facts [] [] = ""
@@ -425,8 +424,8 @@
end
fun of_free (s, T) =
- maybe_quote keywords s ^ " :: " ^
- maybe_quote keywords (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
+ Proof_Context.print_name ctxt s ^ " :: " ^
+ maybe_quote ctxt (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
fun add_frees xs (s, ctxt) =
(s ^ space_implode " and " (map of_free xs), ctxt |> fold Proof_Context.augment (map Free xs))
--- a/src/HOL/ex/Sketch_and_Explore.thy Wed Mar 06 09:43:25 2024 +0100
+++ b/src/HOL/ex/Sketch_and_Explore.thy Tue Feb 27 13:46:42 2024 +0100
@@ -18,7 +18,7 @@
in (fixes, assms, concl) end;
fun maybe_quote ctxt =
- ATP_Util.maybe_quote (Thy_Header.get_keywords' ctxt);
+ ATP_Util.maybe_quote ctxt;
fun print_typ ctxt T =
T