more flexible command syntax;

--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Sep 29 21:20:36 2024 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Sep 29 21:40:37 2024 +0200
@@ -1112,7 +1112,7 @@
     ;
     mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')')
     ;
-    syntaxdeps: (@{syntax name}+) ('==' | '\<rightleftharpoons>') (@{syntax name}+)
+    syntaxdeps: (((@{syntax name}+) ('==' | '\<rightleftharpoons>'))?) (@{syntax name}+)
     ;
     transpat: ('(' @{syntax name} ')')? @{syntax string}
   \<close>
@@ -1173,6 +1173,10 @@
   specification of the effect of translation rules (see below) or translation
   functions (see \secref{sec:tr-funs}).
 
+  @{command "syntax_types"}~\<open>types\<close> and @{command "syntax_consts"}~\<open>consts\<close>
+  merely declare formal entities to the inner-syntax engine, without any
+  dependencies yet.
+
   \<^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

--- a/src/Pure/Pure.thy	Sun Sep 29 21:20:36 2024 +0200
+++ b/src/Pure/Pure.thy	Sun Sep 29 21:40:37 2024 +0200
@@ -404,7 +404,7 @@
 
 val syntax_consts =
   Parse.and_list1
-    ((Scan.repeat1 Parse.name_position --| (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) --
+    (Scan.optional (Scan.repeat1 Parse.name_position --| (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) [] --
       Parse.!!! (Scan.repeat1 Parse.name_position));
 
 val _ =