# HG changeset patch
# User wenzelm
# Date 1729109224 -7200
# Node ID 8e7bd056675995282f51427f52b820981cded778
# Parent  137ea3d464be27201602a1944bc0246073f86674
show_consts_markup is enabled by default;

diff -r 137ea3d464be -r 8e7bd0566759 NEWS
--- 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
diff -r 137ea3d464be -r 8e7bd0566759 src/Doc/Isar_Ref/Inner_Syntax.thy
--- 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
diff -r 137ea3d464be -r 8e7bd0566759 src/Pure/Syntax/printer.ML
--- 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);