src/Doc/Isar_Ref/Document_Preparation.thy

   to indicate some modification in the way it is printed in the document.
 
   @{rail \<open>
     @{syntax_def tags}: ( tag * )
     ;
-    tag: '%' (@{syntax ident} | @{syntax string})
+    tag: '%' (@{syntax short_ident} | @{syntax string})
   \<close>}
 
   Some tags are pre-declared for certain classes of commands, serving as
   default markup if no tags are given in the text:
 

     '@'? (string | @{syntax antiquotation}) |
     '\<newline>'
   \<close>}
   \endgroup
 
-  The lexical syntax of \<open>identifier\<close> coincides with that of @{syntax ident} in
-  regular Isabelle syntax, but \<open>string\<close> uses single quotes instead of double
-  quotes of the standard @{syntax string} category.
+  The lexical syntax of \<open>identifier\<close> coincides with that of @{syntax
+  short_ident} in regular Isabelle syntax, but \<open>string\<close> uses single quotes
+  instead of double quotes of the standard @{syntax string} category.
 
   Each \<open>rule\<close> defines a formal language (with optional name), using a notation
   that is similar to EBNF or regular expressions with recursion. The meaning
   and visual appearance of these rail language elements is illustrated by the
   following representative examples.