allow type constraints for const_syntax;
cope with that in ast translations and mixfix templates;
minor adjustments to print_ast_translation functions in ML;

--- a/NEWS	Tue Oct 15 12:18:02 2024 +0200
+++ b/NEWS	Tue Oct 15 14:19:58 2024 +0200
@@ -46,6 +46,14 @@
 hyperlinks work properly e.g. for "['a, 'b] \<Rightarrow> 'c" or "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> C" in
 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.
+
 * The Simplifier now supports special "congprocs", using keyword
 'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML
 antiquotation of the same name). See also

--- a/src/Pure/Isar/attrib.ML	Tue Oct 15 12:18:02 2024 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Oct 15 14:19:58 2024 +0200
@@ -606,6 +606,7 @@
   register_config_bool Printer.show_sorts #>
   register_config_bool Printer.show_types #>
   register_config_bool Printer.show_markup #>
+  register_config_bool Printer.show_consts_markup #>
   register_config_bool Printer.show_structs #>
   register_config_bool Printer.show_question_marks #>
   register_config_bool Syntax.ambiguity_warning #>

--- a/src/Pure/Syntax/ast.ML	Tue Oct 15 12:18:02 2024 +0200
+++ b/src/Pure/Syntax/ast.ML	Tue Oct 15 14:19:58 2024 +0200
@@ -137,13 +137,16 @@
 fun fold_ast_p c = uncurry (fold_rev (fn x => fn xs => Appl [Constant c, x, xs]));
 
 
-fun unfold_ast c (y as Appl [Constant c', x, xs]) =
+fun unfold_ast c (y as Appl [Appl [Constant "_constrain", Constant c', _], x, xs]) =
+      if c = c' then x :: unfold_ast c xs else [y]
+  | unfold_ast c (y as Appl [Constant c', x, xs]) =
       if c = c' then x :: unfold_ast c xs else [y]
   | unfold_ast _ y = [y];
 
-fun unfold_ast_p c (y as Appl [Constant c', x, xs]) =
-      if c = c' then apfst (cons x) (unfold_ast_p c xs)
-      else ([], y)
+fun unfold_ast_p c (y as Appl [Appl [Constant "_constrain", Constant c', _], x, xs]) =
+      if c = c' then apfst (cons x) (unfold_ast_p c xs) else ([], y)
+  | unfold_ast_p c (y as Appl [Constant c', x, xs]) =
+      if c = c' then apfst (cons x) (unfold_ast_p c xs) else ([], y)
   | unfold_ast_p _ y = ([], y);
 
 
@@ -156,8 +159,12 @@
 
 exception NO_MATCH;
 
-fun match1 (Constant a) (Constant b) env = if a = b then env else raise NO_MATCH
-  | match1 (Variable a) (Constant b) env = if a = b then env else raise NO_MATCH
+fun const_match (Constant a) b = a = b
+  | const_match (Variable a) b = a = b
+  | const_match (Appl [Constant "_constrain", ast, _]) b = const_match ast b
+  | const_match _ _ = false;
+
+fun match1 ast (Constant b) env = if const_match ast b then env else raise NO_MATCH
   | match1 ast (Variable x) env = Symtab.update (x, ast) env
   | match1 (Appl asts) (Appl pats) env = match2 asts pats env
   | match1 _ _ _ = raise NO_MATCH
@@ -195,6 +202,8 @@
 
 fun head_name (Constant a) = SOME a
   | head_name (Variable a) = SOME a
+  | head_name (Appl [Constant "_constrain", Constant a, _]) = SOME a
+  | head_name (Appl (Appl [Constant "_constrain", Constant a, _] :: _)) = SOME a
   | head_name (Appl (Constant a :: _)) = SOME a
   | head_name (Appl (Variable a :: _)) = SOME a
   | head_name _ = NONE;

--- a/src/Pure/Syntax/printer.ML	Tue Oct 15 12:18:02 2024 +0200
+++ b/src/Pure/Syntax/printer.ML	Tue Oct 15 14:19:58 2024 +0200
@@ -10,6 +10,7 @@
   val show_types: bool Config.T
   val show_sorts: bool Config.T
   val show_markup: bool Config.T
+  val show_consts_markup: bool Config.T
   val show_structs: bool Config.T
   val show_question_marks: bool Config.T
   val pretty_priority: int Config.T
@@ -52,6 +53,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_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);
@@ -226,9 +228,21 @@
       else if curried then Syntax_Trans.applC_ast_tr'
       else Syntax_Trans.appl_ast_tr';
 
+    fun constrain_trans (Ast.Appl [Ast.Constant (a as "_constrain"), ast, ty]) =
+          markup_trans a [ast, ty]
+      | constrain_trans _ = NONE;
+
     fun main _ (Ast.Variable x) = [Ast.pretty_var x]
-      | main p (c as Ast.Constant a) = combination p c a []
-      | main p (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _))) = combination p c a args
+      | main p (cc as Ast.Appl [Ast.Constant "_constrain", c as Ast.Constant a, _]) =
+          combination p c a [] (SOME cc)
+      | main p (c as Ast.Constant a) =
+          combination p c a [] NONE
+      | main p
+          (Ast.Appl ((cc as Ast.Appl [Ast.Constant "_constrain", c as Ast.Constant a, _]) ::
+            (args as _ :: _))) =
+          combination p c a args (SOME cc)
+      | main p (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _))) =
+          combination p c a args NONE
       | main p (Ast.Appl (f :: (args as _ :: _))) = main p (application (f, args))
       | main _ (ast as Ast.Appl _) = raise Ast.AST ("pretty: malformed ast", [ast])
 
@@ -240,7 +254,7 @@
           |> Config.put pretty_priority p
           |> pretty) tabs trf markup_trans (markup, extern) ast
 
-    and combination p c a args =
+    and combination p c a args constraint =
       (case translation p a args of
         SOME prts => prts
       | NONE =>
@@ -254,8 +268,11 @@
           in
             (case entry of
               NONE =>
-                if nargs = 0 then [Pretty.marks_str (markup a, extern a)]
-                else main p (application (c, args))
+                if nargs = 0 then
+                  (case Option.mapPartial constrain_trans constraint of
+                    SOME prt => [prt]
+                  | NONE => [Pretty.marks_str (markup a, extern a)])
+                else main p (application (the_default c constraint, args))
             | SOME (symbs, n, q) =>
                 if nargs = n then parens p q a (symbs, args)
                 else main p (application (split_args n [c] args)))

--- a/src/Pure/Syntax/syntax_phases.ML	Tue Oct 15 12:18:02 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Oct 15 14:19:58 2024 +0200
@@ -662,6 +662,7 @@
   let
     val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
     val show_markup = Config.get ctxt show_markup;
+    val show_consts_markup = Config.get ctxt show_consts_markup;
 
     fun constrain_ast clean T ast =
       if T = dummyT then ast
@@ -684,11 +685,18 @@
           in Ast.mk_appl (var_ast (c $ Syntax.free x) X) (map ast_of ts) end
       | (Const ("_idtdummy", T), ts) =>
           Ast.mk_appl (var_ast (Syntax.const "_idtdummy") T) (map ast_of ts)
-      | (Const (c, T), ts) => trans c (Type_Annotation.smash T) ts
+      | (Const (c, T), ts) => const_ast c T ts
       | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
 
-    and trans a T args = ast_of (trf a ctxt T args)
-      handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
+    and const_ast a T args =
+      (case SOME (trf a ctxt (Type_Annotation.smash T) args) handle Match => NONE of
+        SOME t => ast_of t
+      | NONE =>
+          let
+            val c =
+              Ast.Constant a
+              |> (show_markup andalso show_consts_markup) ? constrain_ast {clean = true} T;
+          in Ast.mk_appl c (map ast_of args) end)
 
     and var_ast v T =
       simple_ast_of ctxt v