1.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 21:59:02 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 21:59:47 2008 +0100
     1.3 @@ -68,40 +68,65 @@
     1.4  
     1.5  section {* Lexical matters \label{sec:outer-lex} *}
     1.6  
     1.7 -text {* The Isabelle/Isar outer syntax provides token classes as
     1.8 -  presented below; most of these coincide with the inner lexical
     1.9 -  syntax as defined in \secref{sec:inner-lex}.
    1.10 +text {* The outer lexical syntax consists of three main categories of
    1.11 +  tokens:
    1.12  
    1.13 -  \begin{matharray}{rcl}
    1.14 -    @{syntax_def ident} & = & letter\,quasiletter^* \\
    1.15 -    @{syntax_def longident} & = & ident (\verb,.,ident)^+ \\
    1.16 -    @{syntax_def symident} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\
    1.17 -    @{syntax_def nat} & = & digit^+ \\
    1.18 -    @{syntax_def var} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
    1.19 -    @{syntax_def typefree} & = & \verb,',ident \\
    1.20 -    @{syntax_def typevar} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
    1.21 -    @{syntax_def string} & = & \verb,", ~\dots~ \verb,", \\
    1.22 -    @{syntax_def altstring} & = & \backquote ~\dots~ \backquote \\
    1.23 -    @{syntax_def verbatim} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex]
    1.24 +  \begin{enumerate}
    1.25  
    1.26 -    letter & = & latin ~|~ \verb,\,\verb,<,latin\verb,>, ~|~ \verb,\,\verb,<,latin\,latin\verb,>, ~|~ greek ~|~ \\
    1.27 -           &   & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
    1.28 -    quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
    1.29 -    latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
    1.30 -    digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
    1.31 -    sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~
    1.32 -     \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \\
    1.33 -    & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
    1.34 -    \verb,^, ~|~ \verb,_, ~|~ \verb,|, ~|~ \verb,~, \\
    1.35 -    greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
    1.36 -          &   & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
    1.37 -          &   & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
    1.38 -          &   & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~|~ \verb,\<tau>, ~| \\
    1.39 -          &   & \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<chi>, ~|~ \verb,\<psi>, ~| \\
    1.40 -          &   & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
    1.41 -          &   & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
    1.42 -          &   & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
    1.43 -  \end{matharray}
    1.44 +  \item \emph{major keywords} --- the command names that are available
    1.45 +  in the present logic session;
    1.46 +
    1.47 +  \item \emph{minor keywords} --- additional literal tokens required
    1.48 +  by the syntax of commands;
    1.49 +
    1.50 +  \item \emph{named tokens} --- various categories of identifiers,
    1.51 +  string tokens etc.
    1.52 +
    1.53 +  \end{enumerate}
    1.54 +
    1.55 +  Minor keywords and major keywords are guaranteed to be disjoint.
    1.56 +  This helps user-interfaces to determine the overall structure of a
    1.57 +  theory text, without knowing the full details of command syntax.
    1.58 +
    1.59 +  Keywords override named tokens.  For example, the presence of a
    1.60 +  command called @{verbatim term} inhibits the identifier @{verbatim
    1.61 +  term}, but the string @{verbatim "\"term\""} can be used instead.
    1.62 +  By convention, the outer syntax always allows quoted strings in
    1.63 +  addition to identifiers, wherever a named entity is expected.
    1.64 +
    1.65 +  \medskip The categories for named tokens are defined once and for
    1.66 +  all as follows.
    1.67 +
    1.68 +  \smallskip
    1.69 +  \begin{supertabular}{rcl}
    1.70 +    @{syntax_def ident} & = & @{text "letter quasiletter\<^sup>*"} \\
    1.71 +    @{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\
    1.72 +    @{syntax_def symident} & = & @{text "sym\<^sup>+  |  "}@{verbatim "\\"}@{verbatim "<"}@{text ident}@{verbatim ">"} \\
    1.73 +    @{syntax_def nat} & = & @{text "digit\<^sup>+"} \\
    1.74 +    @{syntax_def var} & = & @{verbatim "?"}@{text "ident  |  "}@{verbatim "?"}@{text ident}@{verbatim "."}@{text nat} \\
    1.75 +    @{syntax_def typefree} & = & @{verbatim "'"}@{text ident} \\
    1.76 +    @{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree  |  "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\
    1.77 +    @{syntax_def string} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
    1.78 +    @{syntax_def altstring} & = & @{verbatim "`"} @{text "\<dots>"} @{verbatim "`"} \\
    1.79 +    @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*"}@{verbatim "}"} \\[1ex]
    1.80 +
    1.81 +    @{text letter} & = & @{text "latin  |  "}@{verbatim "\\"}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text "  |  "}@{verbatim "\\"}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text "  |  greek  |"} \\
    1.82 +          &   & @{verbatim "\<^isub>"}@{text "  |  "}@{verbatim "\<^isup>"} \\
    1.83 +    @{text quasiletter} & = & @{text "letter  |  digit  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "'"} \\
    1.84 +    @{text latin} & = & @{verbatim a}@{text "  | \<dots> |  "}@{verbatim z}@{text "  |  "}@{verbatim A}@{text "  |  \<dots> |  "}@{verbatim Z} \\
    1.85 +    @{text digit} & = & @{verbatim "0"}@{text "  |  \<dots> |  "}@{verbatim "9"} \\
    1.86 +    @{text sym} & = & @{verbatim "!"}@{text "  |  "}@{verbatim "#"}@{text "  |  "}@{verbatim "$"}@{text "  |  "}@{verbatim "%"}@{text "  |  "}@{verbatim "&"}@{text "  |  "}@{verbatim "*"}@{text "  |  "}@{verbatim "+"}@{text "  |  "}@{verbatim "-"}@{text "  |  "}@{verbatim "/"}@{text "  |"} \\
    1.87 +    & & @{verbatim "<"}@{text "  |  "}@{verbatim "="}@{text "  |  "}@{verbatim ">"}@{text "  |  "}@{verbatim "?"}@{text "  |  "}@{verbatim "@"}@{text "  |  "}@{verbatim "^"}@{text "  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "|"}@{text "  |  "}@{verbatim "~"} \\
    1.88 +    @{text greek} & = & @{verbatim "\<alpha>"}@{text "  |  "}@{verbatim "\<beta>"}@{text "  |  "}@{verbatim "\<gamma>"}@{text "  |  "}@{verbatim "\<delta>"}@{text "  |"} \\
    1.89 +          &   & @{verbatim "\<epsilon>"}@{text "  |  "}@{verbatim "\<zeta>"}@{text "  |  "}@{verbatim "\<eta>"}@{text "  |  "}@{verbatim "\<theta>"}@{text "  |"} \\
    1.90 +          &   & @{verbatim "\<iota>"}@{text "  |  "}@{verbatim "\<kappa>"}@{text "  |  "}@{verbatim "\<mu>"}@{text "  |  "}@{verbatim "\<nu>"}@{text "  |"} \\
    1.91 +          &   & @{verbatim "\<xi>"}@{text "  |  "}@{verbatim "\<pi>"}@{text "  |  "}@{verbatim "\<rho>"}@{text "  |  "}@{verbatim "\<sigma>"}@{text "  |  "}@{verbatim "\<tau>"}@{text "  |"} \\
    1.92 +          &   & @{verbatim "\<upsilon>"}@{text "  |  "}@{verbatim "\<phi>"}@{text "  |  "}@{verbatim "\<chi>"}@{text "  |  "}@{verbatim "\<psi>"}@{text "  |"} \\
    1.93 +          &   & @{verbatim "\<omega>"}@{text "  |  "}@{verbatim "\<Gamma>"}@{text "  |  "}@{verbatim "\<Delta>"}@{text "  |  "}@{verbatim "\<Theta>"}@{text "  |"} \\
    1.94 +          &   & @{verbatim "\<Lambda>"}@{text "  |  "}@{verbatim "\<Xi>"}@{text "  |  "}@{verbatim "\<Pi>"}@{text "  |  "}@{verbatim "\<Sigma>"}@{text "  |"} \\
    1.95 +          &   & @{verbatim "\<Upsilon>"}@{text "  |  "}@{verbatim "\<Phi>"}@{text "  |  "}@{verbatim "\<Psi>"}@{text "  |  "}@{verbatim "\<Omega>"} \\
    1.96 +  \end{supertabular}
    1.97 +  \medskip
    1.98  
    1.99    The syntax of @{syntax string} admits any characters, including
   1.100    newlines; ``@{verbatim "\""}'' (double-quote) and ``@{verbatim
   1.101 @@ -123,12 +148,11 @@
   1.102    is given in \cite[appendix~A]{isabelle-sys}.
   1.103    
   1.104    Source comments take the form @{verbatim "(*"}~@{text
   1.105 -  "\<dots>"}~@{verbatim "*)"} and may be nested, although user-interface
   1.106 -  tools might prevent this.  Note that this form indicates source
   1.107 -  comments only, which are stripped after lexical analysis of the
   1.108 -  input.  The Isar syntax also provides proper \emph{document
   1.109 -  comments} that are considered as part of the text (see
   1.110 -  \secref{sec:comments}).
   1.111 +  "\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface
   1.112 +  might prevent this.  Note that this form indicates source comments
   1.113 +  only, which are stripped after lexical analysis of the input.  The
   1.114 +  Isar syntax also provides proper \emph{document comments} that are
   1.115 +  considered as part of the text (see \secref{sec:comments}).
   1.116  *}
   1.117  
   1.118