updated theory header syntax and related details;
authorwenzelm
Mon Mar 26 15:38:09 2012 +0200 (2012-03-26)
changeset 471147c9e31ffcd9e
parent 47113 b5a5662528fb
child 47115 1a05adae1cc9
updated theory header syntax and related details;
doc-src/IsarRef/Thy/Outer_Syntax.thy
doc-src/IsarRef/Thy/Spec.thy
doc-src/IsarRef/Thy/document/Outer_Syntax.tex
doc-src/IsarRef/Thy/document/Spec.tex
     1.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Sat Mar 24 20:24:16 2012 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Mon Mar 26 15:38:09 2012 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4  imports Base Main
     1.5  begin
     1.6  
     1.7 -chapter {* Outer syntax --- the theory language *}
     1.8 +chapter {* Outer syntax --- the theory language \label{ch:outer-syntax} *}
     1.9  
    1.10  text {*
    1.11    The rather generic framework of Isabelle/Isar syntax emerges from
     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Sat Mar 24 20:24:16 2012 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Mon Mar 26 15:38:09 2012 +0200
     2.3 @@ -51,9 +51,12 @@
     2.4    admissible.
     2.5  
     2.6    @{rail "
     2.7 -    @@{command theory} @{syntax name} \\ @'imports' (@{syntax name} +) uses? @'begin'
     2.8 +    @@{command theory} @{syntax name} imports \\ keywords? uses? @'begin'
     2.9      ;
    2.10 -
    2.11 +    imports: @'imports' (@{syntax name} +)
    2.12 +    ;
    2.13 +    keywords: @'keywords' ((@{syntax string} +) ('::' @{syntax name} @{syntax tags})? + @'and')
    2.14 +    ;
    2.15      uses: @'uses' ((@{syntax name} | @{syntax parname}) +)
    2.16    "}
    2.17  
    2.18 @@ -61,17 +64,28 @@
    2.19  
    2.20    \item @{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"}
    2.21    starts a new theory @{text A} based on the merge of existing
    2.22 -  theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.
    2.23 -  
    2.24 -  Due to the possibility to import more than one ancestor, the
    2.25 -  resulting theory structure of an Isabelle session forms a directed
    2.26 -  acyclic graph (DAG).  Isabelle's theory loader ensures that the
    2.27 -  sources contributing to the development graph are always up-to-date:
    2.28 -  changed files are automatically reloaded whenever a theory header
    2.29 -  specification is processed.
    2.30 +  theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.  Due to the possibility to import more
    2.31 +  than one ancestor, the resulting theory structure of an Isabelle
    2.32 +  session forms a directed acyclic graph (DAG).  Isabelle takes care
    2.33 +  that sources contributing to the development graph are always
    2.34 +  up-to-date: changed files are automatically rechecked whenever a
    2.35 +  theory header specification is processed.
    2.36 +
    2.37 +  The optional @{keyword_def "keywords"} specification declares outer
    2.38 +  syntax (\chref{ch:outer-syntax}) that is introduced in this theory
    2.39 +  later on (rare in end-user applications).  Both minor keywords and
    2.40 +  major keywords of the Isar command language need to be specified, in
    2.41 +  order to make parsing of proof documents work properly.  Command
    2.42 +  keywords need to be classified according to their structural role in
    2.43 +  the formal text.  Examples may be seen in Isabelle/HOL sources
    2.44 +  itself, such as @{keyword "keywords"}~@{verbatim "\"typedef\""}
    2.45 +  @{text ":: thy_goal"} or @{keyword "keywords"}~@{verbatim
    2.46 +  "\"datatype\""} @{text ":: thy_decl"} for theory-level declarations
    2.47 +  with and without proof, respectively.  Additional @{syntax tags}
    2.48 +  provide defaults for document preparation (\secref{sec:tags}).
    2.49    
    2.50    The optional @{keyword_def "uses"} specification declares additional
    2.51 -  dependencies on extra files (usually ML sources).  Files will be
    2.52 +  dependencies on external files (notably ML sources).  Files will be
    2.53    loaded immediately (as ML), unless the name is parenthesized.  The
    2.54    latter case records a dependency that needs to be resolved later in
    2.55    the text, usually via explicit @{command_ref "use"} for ML files;
    2.56 @@ -79,8 +93,10 @@
    2.57    corresponding tools or packages.
    2.58    
    2.59    \item @{command (global) "end"} concludes the current theory
    2.60 -  definition.  Note that local theory targets involve a local
    2.61 -  @{command (local) "end"}, which is clear from the nesting.
    2.62 +  definition.  Note that some other commands, e.g.\ local theory
    2.63 +  targets @{command locale} or @{command class} may involve a
    2.64 +  @{keyword "begin"} that needs to be matched by @{command (local)
    2.65 +  "end"}, according to the usual rules for nested blocks.
    2.66  
    2.67    \end{description}
    2.68  *}
     3.1 --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Sat Mar 24 20:24:16 2012 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Mon Mar 26 15:38:09 2012 +0200
     3.3 @@ -18,7 +18,7 @@
     3.4  %
     3.5  \endisadelimtheory
     3.6  %
     3.7 -\isamarkupchapter{Outer syntax --- the theory language%
     3.8 +\isamarkupchapter{Outer syntax --- the theory language \label{ch:outer-syntax}%
     3.9  }
    3.10  \isamarkuptrue%
    3.11  %
     4.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Sat Mar 24 20:24:16 2012 +0100
     4.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Mar 26 15:38:09 2012 +0200
     4.3 @@ -72,18 +72,42 @@
     4.4  \rail@begin{4}{}
     4.5  \rail@term{\hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}}[]
     4.6  \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
     4.7 +\rail@nont{\isa{imports}}[]
     4.8  \rail@cr{2}
     4.9 -\rail@term{\isa{\isakeyword{imports}}}[]
    4.10 -\rail@plus
    4.11 -\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    4.12 -\rail@nextplus{3}
    4.13 -\rail@endplus
    4.14 +\rail@bar
    4.15 +\rail@nextbar{3}
    4.16 +\rail@nont{\isa{keywords}}[]
    4.17 +\rail@endbar
    4.18  \rail@bar
    4.19  \rail@nextbar{3}
    4.20  \rail@nont{\isa{uses}}[]
    4.21  \rail@endbar
    4.22  \rail@term{\isa{\isakeyword{begin}}}[]
    4.23  \rail@end
    4.24 +\rail@begin{2}{\isa{imports}}
    4.25 +\rail@term{\isa{\isakeyword{imports}}}[]
    4.26 +\rail@plus
    4.27 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    4.28 +\rail@nextplus{1}
    4.29 +\rail@endplus
    4.30 +\rail@end
    4.31 +\rail@begin{3}{\isa{keywords}}
    4.32 +\rail@term{\isa{\isakeyword{keywords}}}[]
    4.33 +\rail@plus
    4.34 +\rail@plus
    4.35 +\rail@nont{\hyperlink{syntax.string}{\mbox{\isa{string}}}}[]
    4.36 +\rail@nextplus{1}
    4.37 +\rail@endplus
    4.38 +\rail@bar
    4.39 +\rail@nextbar{1}
    4.40 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
    4.41 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
    4.42 +\rail@nont{\hyperlink{syntax.tags}{\mbox{\isa{tags}}}}[]
    4.43 +\rail@endbar
    4.44 +\rail@nextplus{2}
    4.45 +\rail@cterm{\isa{\isakeyword{and}}}[]
    4.46 +\rail@endplus
    4.47 +\rail@end
    4.48  \rail@begin{3}{\isa{uses}}
    4.49  \rail@term{\isa{\isakeyword{uses}}}[]
    4.50  \rail@plus
    4.51 @@ -102,17 +126,27 @@
    4.52  
    4.53    \item \hyperlink{command.theory}{\mbox{\isa{\isacommand{theory}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C494D504F5254533E}{\isasymIMPORTS}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}}
    4.54    starts a new theory \isa{A} based on the merge of existing
    4.55 -  theories \isa{{\isaliteral{22}{\isachardoublequote}}B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.
    4.56 -  
    4.57 -  Due to the possibility to import more than one ancestor, the
    4.58 -  resulting theory structure of an Isabelle session forms a directed
    4.59 -  acyclic graph (DAG).  Isabelle's theory loader ensures that the
    4.60 -  sources contributing to the development graph are always up-to-date:
    4.61 -  changed files are automatically reloaded whenever a theory header
    4.62 -  specification is processed.
    4.63 +  theories \isa{{\isaliteral{22}{\isachardoublequote}}B\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}.  Due to the possibility to import more
    4.64 +  than one ancestor, the resulting theory structure of an Isabelle
    4.65 +  session forms a directed acyclic graph (DAG).  Isabelle takes care
    4.66 +  that sources contributing to the development graph are always
    4.67 +  up-to-date: changed files are automatically rechecked whenever a
    4.68 +  theory header specification is processed.
    4.69 +
    4.70 +  The optional \indexdef{}{keyword}{keywords}\hypertarget{keyword.keywords}{\hyperlink{keyword.keywords}{\mbox{\isa{\isakeyword{keywords}}}}} specification declares outer
    4.71 +  syntax (\chref{ch:outer-syntax}) that is introduced in this theory
    4.72 +  later on (rare in end-user applications).  Both minor keywords and
    4.73 +  major keywords of the Isar command language need to be specified, in
    4.74 +  order to make parsing of proof documents work properly.  Command
    4.75 +  keywords need to be classified according to their structural role in
    4.76 +  the formal text.  Examples may be seen in Isabelle/HOL sources
    4.77 +  itself, such as \hyperlink{keyword.keywords}{\mbox{\isa{\isakeyword{keywords}}}}~\verb|"typedef"|
    4.78 +  \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ thy{\isaliteral{5F}{\isacharunderscore}}goal{\isaliteral{22}{\isachardoublequote}}} or \hyperlink{keyword.keywords}{\mbox{\isa{\isakeyword{keywords}}}}~\verb|"datatype"| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ thy{\isaliteral{5F}{\isacharunderscore}}decl{\isaliteral{22}{\isachardoublequote}}} for theory-level declarations
    4.79 +  with and without proof, respectively.  Additional \hyperlink{syntax.tags}{\mbox{\isa{tags}}}
    4.80 +  provide defaults for document preparation (\secref{sec:tags}).
    4.81    
    4.82    The optional \indexdef{}{keyword}{uses}\hypertarget{keyword.uses}{\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{uses}}}}} specification declares additional
    4.83 -  dependencies on extra files (usually ML sources).  Files will be
    4.84 +  dependencies on external files (notably ML sources).  Files will be
    4.85    loaded immediately (as ML), unless the name is parenthesized.  The
    4.86    latter case records a dependency that needs to be resolved later in
    4.87    the text, usually via explicit \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} for ML files;
    4.88 @@ -120,8 +154,9 @@
    4.89    corresponding tools or packages.
    4.90    
    4.91    \item \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} concludes the current theory
    4.92 -  definition.  Note that local theory targets involve a local
    4.93 -  \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}, which is clear from the nesting.
    4.94 +  definition.  Note that some other commands, e.g.\ local theory
    4.95 +  targets \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} may involve a
    4.96 +  \hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} that needs to be matched by \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}}, according to the usual rules for nested blocks.
    4.97  
    4.98    \end{description}%
    4.99  \end{isamarkuptext}%