# HG changeset patch
# User wenzelm
# Date 1464098583 -7200
# Node ID 70f4d67235a0471b93d0bbf50c80f33b4df86429
# Parent  9553f11d67c46e3eedb7f98dac93a8f766cbf6d6
clarified syntax category names according to Isabelle/ML/Scala;

diff -r 9553f11d67c4 -r 70f4d67235a0 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Tue May 24 15:53:16 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Tue May 24 16:03:03 2016 +0200
@@ -462,7 +462,7 @@
   @{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
@@ -538,9 +538,9 @@
   \<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
diff -r 9553f11d67c4 -r 70f4d67235a0 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue May 24 15:53:16 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue May 24 16:03:03 2016 +0200
@@ -387,7 +387,7 @@
     ;
     entry: atom ('=' atom)?
     ;
-    atom: @{syntax ident} | @{syntax int} | @{syntax float} | @{syntax cartouche}
+    atom: @{syntax short_ident} | @{syntax int} | @{syntax float} | @{syntax cartouche}
   \<close>}
 
   Each @{syntax entry} is a name-value pair: if the value is omitted, if
@@ -556,11 +556,11 @@
 
   \begin{center}
   \begin{supertabular}{rcl}
-    @{syntax_def (inner) id} & = & @{syntax_ref ident} \\
-    @{syntax_def (inner) longid} & = & @{syntax_ref longident} \\
+    @{syntax_def (inner) id} & = & @{syntax_ref short_ident} \\
+    @{syntax_def (inner) longid} & = & @{syntax_ref long_ident} \\
     @{syntax_def (inner) var} & = & @{syntax_ref var} \\
-    @{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
-    @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
+    @{syntax_def (inner) tid} & = & @{syntax_ref type_ident} \\
+    @{syntax_def (inner) tvar} & = & @{syntax_ref type_var} \\
     @{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\
     @{syntax_def (inner) float_token} & = & @{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat} \\
     @{syntax_def (inner) str_token} & = & \<^verbatim>\<open>''\<close> \<open>\<dots>\<close> \<^verbatim>\<open>''\<close> \\
diff -r 9553f11d67c4 -r 70f4d67235a0 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue May 24 15:53:16 2016 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue May 24 16:03:03 2016 +0200
@@ -97,14 +97,14 @@
 
   \begin{center}
   \begin{supertabular}{rcl}
-    @{syntax_def ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\
-    @{syntax_def longident} & = & \<open>ident(\<close>\<^verbatim>\<open>.\<close>\<open>ident)\<^sup>+\<close> \\
-    @{syntax_def symident} & = & \<open>sym\<^sup>+  |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close> \\
+    @{syntax_def short_ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\
+    @{syntax_def long_ident} & = & \<open>short_ident(\<close>\<^verbatim>\<open>.\<close>\<open>short_ident)\<^sup>+\<close> \\
+    @{syntax_def sym_ident} & = & \<open>sym\<^sup>+  |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>short_ident\<close>\<^verbatim>\<open>>\<close> \\
     @{syntax_def nat} & = & \<open>digit\<^sup>+\<close> \\
     @{syntax_def float} & = & @{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat}~~\<open>|\<close>~~\<^verbatim>\<open>-\<close>@{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat} \\
-    @{syntax_def var} & = & \<^verbatim>\<open>?\<close>\<open>ident  |\<close>~~\<^verbatim>\<open>?\<close>\<open>ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
-    @{syntax_def typefree} & = & \<^verbatim>\<open>'\<close>\<open>ident\<close> \\
-    @{syntax_def typevar} & = & \<^verbatim>\<open>?\<close>\<open>typefree  |\<close>~~\<^verbatim>\<open>?\<close>\<open>typefree\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
+    @{syntax_def term_var} & = & \<^verbatim>\<open>?\<close>\<open>short_ident  |\<close>~~\<^verbatim>\<open>?\<close>\<open>short_ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
+    @{syntax_def type_ident} & = & \<^verbatim>\<open>'\<close>\<open>short_ident\<close> \\
+    @{syntax_def type_var} & = & \<^verbatim>\<open>?\<close>\<open>type_ident  |\<close>~~\<^verbatim>\<open>?\<close>\<open>type_ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
     @{syntax_def string} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\
     @{syntax_def altstring} & = & \<^verbatim>\<open>`\<close> \<open>\<dots>\<close> \<^verbatim>\<open>`\<close> \\
     @{syntax_def cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
@@ -128,13 +128,13 @@
   \end{supertabular}
   \end{center}
 
-  A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown, which is
-  internally a pair of base name and index (ML type @{ML_type indexname}).
-  These components are either separated by a dot as in \<open>?x.1\<close> or \<open>?x7.3\<close> or
-  run together as in \<open>?x1\<close>. The latter form is possible if the base name does
-  not end with digits. If the index is 0, it may be dropped altogether: \<open>?x\<close>
-  and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the same unknown, with basename \<open>x\<close> and
-  index 0.
+  A @{syntax_ref term_var} or @{syntax_ref type_var} describes an unknown,
+  which is internally a pair of base name and index (ML type @{ML_type
+  indexname}). These components are either separated by a dot as in \<open>?x.1\<close> or
+  \<open>?x7.3\<close> or run together as in \<open>?x1\<close>. The latter form is possible if the base
+  name does not end with digits. If the index is 0, it may be dropped
+  altogether: \<open>?x\<close> and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the same unknown, with
+  basename \<open>x\<close> and index 0.
 
   The syntax of @{syntax_ref string} admits any characters, including
   newlines; ``\<^verbatim>\<open>"\<close>'' (double-quote) and ``\<^verbatim>\<open>\\<close>'' (backslash) need to be
@@ -183,8 +183,8 @@
   those ruled out by outer syntax keywords (e.g.\ quoted \<^verbatim>\<open>"let"\<close>).
 
   @{rail \<open>
-    @{syntax_def name}: @{syntax ident} | @{syntax longident} |
-      @{syntax symident} | @{syntax nat} | @{syntax string}
+    @{syntax_def name}: @{syntax short_ident} | @{syntax long_ident} |
+      @{syntax sym_ident} | @{syntax nat} | @{syntax string}
     ;
     @{syntax_def par_name}: '(' @{syntax name} ')'
   \<close>}
@@ -221,8 +221,8 @@
 
   @{rail \<open>
     @{syntax_def embedded}: @{syntax cartouche} | @{syntax string} |
-      @{syntax ident} | @{syntax longident} | @{syntax symident} |
-      @{syntax var} | @{syntax typefree} | @{syntax typevar} | @{syntax nat}
+      @{syntax short_ident} | @{syntax long_ident} | @{syntax sym_ident} |
+      @{syntax term_var} | @{syntax type_ident} | @{syntax type_var} | @{syntax nat}
   \<close>}
 \<close>
 
@@ -304,7 +304,7 @@
     ;
     @{syntax_def named_insts}: (named_inst @'and' +)
     ;
-    variable: @{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}
+    variable: @{syntax name} | @{syntax term_var} | @{syntax type_ident} | @{syntax type_var}
   \<close>}
 
   Type declarations and definitions usually refer to @{syntax typespec} on the
@@ -314,11 +314,11 @@
 
   @{rail \<open>
     @{syntax_def typespec}:
-      (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name}
+      (() | @{syntax type_ident} | '(' ( @{syntax type_ident} + ',' ) ')') @{syntax name}
     ;
     @{syntax_def typespec_sorts}:
-      (() | (@{syntax typefree} ('::' @{syntax sort})?) |
-        '(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
+      (() | (@{syntax type_ident} ('::' @{syntax sort})?) |
+        '(' ( (@{syntax type_ident} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
   \<close>}
 \<close>
 
@@ -386,11 +386,11 @@
   The attribute argument specifications may be any sequence of atomic entities
   (identifiers, strings etc.), or properly bracketed argument lists. Below
   @{syntax atom} refers to any atomic entity, including any @{syntax keyword}
-  conforming to @{syntax symident}.
+  conforming to @{syntax sym_ident}.
 
   @{rail \<open>
-    @{syntax_def atom}: @{syntax name} | @{syntax typefree} |
-      @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
+    @{syntax_def atom}: @{syntax name} | @{syntax type_ident} |
+      @{syntax type_var} | @{syntax term_var} | @{syntax nat} | @{syntax float} |
       @{syntax keyword} | @{syntax cartouche}
     ;
     arg: @{syntax atom} | '(' @{syntax args} ')' | '[' @{syntax args} ']'