# HG changeset patch # User wenzelm # Date 1340219915 -7200 # Node ID 55c305e29f4bca7e2ca1699d7493555d0eb483af # Parent 8537313dd26110da99217587434db172683165dc cover @{class_syntax}, @{type_syntax}, @{const_syntax}, @{syntax_const} in isar-ref, in contrast to other ML antiquotations in implementation manual; diff -r 8537313dd261 -r 55c305e29f4b doc-src/IsarImplementation/Thy/Syntax.thy --- 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 diff -r 8537313dd261 -r 55c305e29f4b doc-src/IsarImplementation/Thy/document/Syntax.tex --- 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 diff -r 8537313dd261 -r 55c305e29f4b doc-src/IsarRef/Thy/Inner_Syntax.thy --- 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 \ theory"} \\ @{command_def "typed_print_translation"} & : & @{text "theory \ theory"} \\ @{command_def "print_ast_translation"} & : & @{text "theory \ 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 diff -r 8537313dd261 -r 55c305e29f4b doc-src/IsarRef/Thy/document/Inner_Syntax.tex --- 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% %