--- a/NEWS Wed Oct 16 21:41:05 2024 +0200
+++ b/NEWS Wed Oct 16 22:07:04 2024 +0200
@@ -47,12 +47,13 @@
Pure, and "\<forall>x\<in>A. B x" or "\<exists>x\<in>A. B x" in HOL.
* Inner syntax printing now supports type constraints for constants:
-this is guarded by the configuration option "show_consts_markup". Ast
-translation rules (command 'translations') and mixfix notation work with
-or without such extra constraints, but ML translation functions (command
-'print_ast_translation') need may need to be changed slightly. Rare
-INCOMPATIBILITY. The Prover IDE displays type constraints for constants
-as for variables, e.g. via C-mouse hovering.
+this is guarded by the configuration options "show_consts_markup"
+(default true) and "show_markup" (default true for PIDE interaction).
+Ast translation rules (command 'translations') and mixfix notation work
+with or without such extra constraints, but ML translation functions
+(command 'print_ast_translation') need may need to be changed slightly.
+Rare INCOMPATIBILITY. The Prover IDE displays type constraints for
+constants as for variables, e.g. via C-mouse hovering.
* The Simplifier now supports special "congprocs", using keyword
'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Oct 16 21:41:05 2024 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Oct 16 22:07:04 2024 +0200
@@ -112,6 +112,7 @@
text \<open>
\begin{tabular}{rcll}
@{attribute_def show_markup} & : & \<open>attribute\<close> \\
+ @{attribute_def show_consts_markup} & : & \<open>attribute\<close> & default \<open>true\<close> \\
@{attribute_def show_types} & : & \<open>attribute\<close> & default \<open>false\<close> \\
@{attribute_def show_sorts} & : & \<open>attribute\<close> & default \<open>false\<close> \\
@{attribute_def show_consts} & : & \<open>attribute\<close> & default \<open>false\<close> \\
@@ -139,6 +140,9 @@
tooltips or popups while hovering with the mouse over the output window, for
example. Consequently, this option is enabled by default for Isabelle/jEdit.
+ \<^descr> @{attribute show_consts_markup} controls printing of type constrains for
+ term constants; this requires @{attribute show_markup}.
+
\<^descr> @{attribute show_types} and @{attribute show_sorts} control printing of
type constraints for term variables, and sort constraints for type
variables. By default, neither of these are shown in output. If @{attribute
--- a/src/Pure/Syntax/printer.ML Wed Oct 16 21:41:05 2024 +0200
+++ b/src/Pure/Syntax/printer.ML Wed Oct 16 22:07:04 2024 +0200
@@ -51,7 +51,7 @@
val show_sorts = Config.declare_option_bool ("show_sorts", \<^here>);
val show_markup_default = Unsynchronized.ref false;
val show_markup = Config.declare_bool ("show_markup", \<^here>) (fn _ => ! show_markup_default);
-val show_consts_markup = Config.declare_bool ("show_consts_markup", \<^here>) (K false);
+val show_consts_markup = Config.declare_bool ("show_consts_markup", \<^here>) (K true);
val show_structs = Config.declare_bool ("show_structs", \<^here>) (K false);
val show_question_marks = Config.declare_option_bool ("show_question_marks", \<^here>);
val show_type_emphasis = Config.declare_bool ("show_type_emphasis", \<^here>) (K true);