NEWS and documentation;

--- a/NEWS	Sun Aug 25 23:19:33 2024 +0200
+++ b/NEWS	Mon Aug 26 13:15:34 2024 +0200
@@ -9,6 +9,13 @@
 
 ** General **
 
+* Inner syntax translations now support formal dependencies via commands
+'syntax_types' or 'syntax_consts'. This is essentially an abstract
+specification of the effect of 'translations' (or translation functions
+in ML). Most Isabelle theories have been adapted accordingly, such that
+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.
+
 * 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/Doc/Isar_Ref/Inner_Syntax.thy	Sun Aug 25 23:19:33 2024 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Aug 26 13:15:34 2024 +0200
@@ -1078,6 +1078,8 @@
     @{command_def "nonterminal"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def "syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     @{command_def "no_syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+    @{command_def "syntax_types"} & : & \<open>theory \<rightarrow> theory\<close> \\
+    @{command_def "syntax_consts"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def "translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def "no_translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{attribute_def syntax_ast_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
@@ -1089,8 +1091,9 @@
   raw syntax declarations provide full access to the priority grammar of the
   inner syntax, without any sanity checks. This includes additional syntactic
   categories (via @{command nonterminal}) and free-form grammar productions
-  (via @{command syntax}). Additional syntax translations (or macros, via
-  @{command translations}) are required to turn resulting parse trees into
+  (via @{command syntax} with formal dependencies via @{command syntax_types}
+  and @{command syntax_consts}). Additional syntax translations (or macros,
+  via @{command translations}) are required to turn resulting parse trees into
   proper representations of formal entities again.
 
   \<^rail>\<open>
@@ -1098,6 +1101,8 @@
     ;
     (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (constdecl +)
     ;
+    (@@{command syntax_types} | @@{command syntax_consts}) (syntaxdeps + @'and')
+    ;
     (@@{command translations} | @@{command no_translations})
       (transpat ('==' | '=>' | '<=' | '\<rightleftharpoons>' | '\<rightharpoonup>' | '\<leftharpoondown>') transpat +)
     ;
@@ -1106,6 +1111,8 @@
     ;
     mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
     ;
+    syntaxdeps: (@{syntax name}+) ('==' | '\<rightleftharpoons>') (@{syntax name}+)
+    ;
     transpat: ('(' @{syntax name} ')')? @{syntax string}
   \<close>
 
@@ -1157,6 +1164,14 @@
   translations) resulting from \<open>decls\<close>, which are interpreted in the same
   manner as for @{command "syntax"} above.
 
+  \<^descr> @{command "syntax_types"}~\<open>syntax \<rightleftharpoons> types\<close> and @{command
+  "syntax_consts"}~\<open>syntax \<rightleftharpoons> consts\<close> declare dependencies of syntax constants
+  wrt.\ formal entities of the logic: multiple names may be given on both
+  sides. This tells the inner-syntax engine how to markup concrete syntax, to
+  support hyperlinks in the browser or editor. It is essentially an abstract
+  specification of the effect of translation rules (see below) or translation
+  functions (see \secref{sec:tr-funs}).
+
   \<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic translation rules
   (i.e.\ macros) as first-order rewrite rules on ASTs (\secref{sec:ast}). The
   theory context maintains two independent lists translation rules: parse