cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual;

--- a/doc-src/IsarImplementation/Thy/Syntax.thy	Wed Jun 20 20:50:04 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/Syntax.thy	Wed Jun 20 21:18:35 2012 +0200
@@ -160,31 +160,4 @@
   \end{description}
 *}
 
-
-section {* Syntax translations *}
-
-text FIXME
-
-text %mlantiq {*
-  \begin{matharray}{rcl}
-  @{ML_antiquotation_def "class_syntax"} & : & @{text ML_antiquotation} \\
-  @{ML_antiquotation_def "type_syntax"} & : & @{text ML_antiquotation} \\
-  @{ML_antiquotation_def "const_syntax"} & : & @{text ML_antiquotation} \\
-  @{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\
-  \end{matharray}
-
-  @{rail "
-  (@@{ML_antiquotation class_syntax} |
-   @@{ML_antiquotation type_syntax} |
-   @@{ML_antiquotation const_syntax} |
-   @@{ML_antiquotation syntax_const}) name
-  "}
-
-  \begin{description}
-
-  \item FIXME
-
-  \end{description}
-*}
-
 end

--- a/doc-src/IsarImplementation/Thy/document/Syntax.tex	Wed Jun 20 20:50:04 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex	Wed Jun 20 21:18:35 2012 +0200
@@ -228,60 +228,6 @@
 %
 \endisadelimmlref
 %
-\isamarkupsection{Syntax translations%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlantiq
-%
-\endisadelimmlantiq
-%
-\isatagmlantiq
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
-  \indexdef{}{ML antiquotation}{class\_syntax}\hypertarget{ML antiquotation.class-syntax}{\hyperlink{ML antiquotation.class-syntax}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}syntax}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
-  \indexdef{}{ML antiquotation}{type\_syntax}\hypertarget{ML antiquotation.type-syntax}{\hyperlink{ML antiquotation.type-syntax}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}syntax}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
-  \indexdef{}{ML antiquotation}{const\_syntax}\hypertarget{ML antiquotation.const-syntax}{\hyperlink{ML antiquotation.const-syntax}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}syntax}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
-  \indexdef{}{ML antiquotation}{syntax\_const}\hypertarget{ML antiquotation.syntax-const}{\hyperlink{ML antiquotation.syntax-const}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}const}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
-  \end{matharray}
-
-  \begin{railoutput}
-\rail@begin{4}{}
-\rail@bar
-\rail@term{\hyperlink{ML antiquotation.class-syntax}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{ML antiquotation.type-syntax}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
-\rail@nextbar{2}
-\rail@term{\hyperlink{ML antiquotation.const-syntax}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
-\rail@nextbar{3}
-\rail@term{\hyperlink{ML antiquotation.syntax-const}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}const}}}}[]
-\rail@endbar
-\rail@nont{\isa{name}}[]
-\rail@end
-\end{railoutput}
-
-
-  \begin{description}
-
-  \item FIXME
-
-  \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlantiq
-{\isafoldmlantiq}%
-%
-\isadelimmlantiq
-%
-\endisadelimmlantiq
-%
 \isadelimtheory
 %
 \endisadelimtheory

--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Jun 20 20:50:04 2012 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Jun 20 21:18:35 2012 +0200
@@ -1438,6 +1438,10 @@
     @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{ML_antiquotation_def "class_syntax"} & : & @{text ML_antiquotation} \\
+    @{ML_antiquotation_def "type_syntax"} & : & @{text ML_antiquotation} \\
+    @{ML_antiquotation_def "const_syntax"} & : & @{text ML_antiquotation} \\
+    @{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
   Syntax translation functions written in ML admit almost arbitrary
@@ -1448,14 +1452,22 @@
   ( @@{command parse_ast_translation} | @@{command parse_translation} |
     @@{command print_translation} | @@{command typed_print_translation} |
     @@{command print_ast_translation}) ('(' @'advanced' ')')? @{syntax text}
+  ;
+  (@@{ML_antiquotation class_syntax} |
+   @@{ML_antiquotation type_syntax} |
+   @@{ML_antiquotation const_syntax} |
+   @@{ML_antiquotation syntax_const}) name
   "}
 
-  Any of the above commands have a single @{syntax text} argument that
-  refers to an ML expression of appropriate type, which are as follows
-  by default:
+  \begin{description}
+
+  \item @{command parse_translation} etc. declare syntax translation
+  functions to the theory.  Any of these commands have a single
+  @{syntax text} argument that refers to an ML expression of
+  appropriate type, which are as follows by default:
 
   \medskip
-  {\small
+  {\footnotesize
   \begin{tabular}{ll}
   @{command parse_ast_translation} & : @{ML_type "(string * (Ast.ast list -> Ast.ast)) list"} \\
   @{command parse_translation} & : @{ML_type "(string * (term list -> term)) list"} \\
@@ -1481,8 +1493,25 @@
   theory or proof context as additional argument.  This allows to
   implement advanced syntax mechanisms, as translations functions may
   refer to specific theory declarations or auxiliary proof data.
+
+  \item @{text "@{class_syntax c}"}, @{text "@{type_syntax c}"},
+  @{text "@{const_syntax c}"} inline the authentic syntax name of the
+  given formal entities into the ML source.  This is the
+  fully-qualified logical name prefixed by a special marker to
+  indicate its kind: thus different logical name spaces are properly
+  distinguished within parse trees.
+
+  \item @{text "@{const_syntax c}"} inlines the name @{text "c"} of
+  the given syntax constant, having checked that it has been declared
+  via some @{command syntax} commands within the theory context.  Note
+  that the usual naming convention makes syntax constants start with
+  underscore, to reduce the chance of accidental clashes with other
+  names occurring in parse trees (unqualified constants etc.).
+
+  \end{description}
 *}
 
+
 subsubsection {* The translation strategy *}
 
 text {* The different kinds of translation functions are called during

--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Jun 20 20:50:04 2012 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Jun 20 21:18:35 2012 +0200
@@ -1683,6 +1683,10 @@
     \indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isaliteral{5F}{\isacharunderscore}}print{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
     \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ theory{\isaliteral{22}{\isachardoublequote}}} \\
+    \indexdef{}{ML antiquotation}{class\_syntax}\hypertarget{ML antiquotation.class-syntax}{\hyperlink{ML antiquotation.class-syntax}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}syntax}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
+    \indexdef{}{ML antiquotation}{type\_syntax}\hypertarget{ML antiquotation.type-syntax}{\hyperlink{ML antiquotation.type-syntax}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}syntax}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
+    \indexdef{}{ML antiquotation}{const\_syntax}\hypertarget{ML antiquotation.const-syntax}{\hyperlink{ML antiquotation.const-syntax}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}syntax}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
+    \indexdef{}{ML antiquotation}{syntax\_const}\hypertarget{ML antiquotation.syntax-const}{\hyperlink{ML antiquotation.syntax-const}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}const}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
   \end{matharray}
 
   Syntax translation functions written in ML admit almost arbitrary
@@ -1710,15 +1714,30 @@
 \rail@endbar
 \rail@nont{\hyperlink{syntax.text}{\mbox{\isa{text}}}}[]
 \rail@end
+\rail@begin{4}{}
+\rail@bar
+\rail@term{\hyperlink{ML antiquotation.class-syntax}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{ML antiquotation.type-syntax}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
+\rail@nextbar{2}
+\rail@term{\hyperlink{ML antiquotation.const-syntax}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
+\rail@nextbar{3}
+\rail@term{\hyperlink{ML antiquotation.syntax-const}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}const}}}}[]
+\rail@endbar
+\rail@nont{\isa{name}}[]
+\rail@end
 \end{railoutput}
 
 
-  Any of the above commands have a single \hyperlink{syntax.text}{\mbox{\isa{text}}} argument that
-  refers to an ML expression of appropriate type, which are as follows
-  by default:
+  \begin{description}
+
+  \item \hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}translation}}}} etc. declare syntax translation
+  functions to the theory.  Any of these commands have a single
+  \hyperlink{syntax.text}{\mbox{\isa{text}}} argument that refers to an ML expression of
+  appropriate type, which are as follows by default:
 
   \medskip
-  {\small
+  {\footnotesize
   \begin{tabular}{ll}
   \hyperlink{command.parse-ast-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}ast{\isaliteral{5F}{\isacharunderscore}}translation}}}} & : \verb|(string * (Ast.ast list -> Ast.ast)) list| \\
   \hyperlink{command.parse-translation}{\mbox{\isa{\isacommand{parse{\isaliteral{5F}{\isacharunderscore}}translation}}}} & : \verb|(string * (term list -> term)) list| \\
@@ -1741,7 +1760,23 @@
   given, the corresponding translation functions depend on the current
   theory or proof context as additional argument.  This allows to
   implement advanced syntax mechanisms, as translations functions may
-  refer to specific theory declarations or auxiliary proof data.%
+  refer to specific theory declarations or auxiliary proof data.
+
+  \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}class{\isaliteral{5F}{\isacharunderscore}}syntax\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}type{\isaliteral{5F}{\isacharunderscore}}syntax\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}},
+  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}const{\isaliteral{5F}{\isacharunderscore}}syntax\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} inline the authentic syntax name of the
+  given formal entities into the ML source.  This is the
+  fully-qualified logical name prefixed by a special marker to
+  indicate its kind: thus different logical name spaces are properly
+  distinguished within parse trees.
+
+  \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}const{\isaliteral{5F}{\isacharunderscore}}syntax\ c{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} inlines the name \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{22}{\isachardoublequote}}} of
+  the given syntax constant, having checked that it has been declared
+  via some \hyperlink{command.syntax}{\mbox{\isa{\isacommand{syntax}}}} commands within the theory context.  Note
+  that the usual naming convention makes syntax constants start with
+  underscore, to reduce the chance of accidental clashes with other
+  names occurring in parse trees (unqualified constants etc.).
+
+  \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %