1.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 21:59:47 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 22:00:12 2008 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4  section {* Lexical matters \label{sec:outer-lex} *}
     1.5  
     1.6  text {* The outer lexical syntax consists of three main categories of
     1.7 -  tokens:
     1.8 +  syntax tokens:
     1.9  
    1.10    \begin{enumerate}
    1.11  
    1.12 @@ -79,14 +79,16 @@
    1.13    \item \emph{minor keywords} --- additional literal tokens required
    1.14    by the syntax of commands;
    1.15  
    1.16 -  \item \emph{named tokens} --- various categories of identifiers,
    1.17 -  string tokens etc.
    1.18 +  \item \emph{named tokens} --- various categories of identifiers etc.
    1.19  
    1.20    \end{enumerate}
    1.21  
    1.22 -  Minor keywords and major keywords are guaranteed to be disjoint.
    1.23 +  Major keywords and minor keywords are guaranteed to be disjoint.
    1.24    This helps user-interfaces to determine the overall structure of a
    1.25    theory text, without knowing the full details of command syntax.
    1.26 +  Internally, there is some additional information about the kind of
    1.27 +  major keywords, which approximates the command type (theory command,
    1.28 +  proof command etc.).
    1.29  
    1.30    Keywords override named tokens.  For example, the presence of a
    1.31    command called @{verbatim term} inhibits the identifier @{verbatim
    1.32 @@ -94,10 +96,15 @@
    1.33    By convention, the outer syntax always allows quoted strings in
    1.34    addition to identifiers, wherever a named entity is expected.
    1.35  
    1.36 +  When tokenizing a given input sequence, the lexer repeatedly takes
    1.37 +  the longest prefix of the input that forms a valid token.  Spaces,
    1.38 +  tabs, newlines and formfeeds between tokens serve as explicit
    1.39 +  separators.
    1.40 +
    1.41    \medskip The categories for named tokens are defined once and for
    1.42    all as follows.
    1.43  
    1.44 -  \smallskip
    1.45 +  \begin{center}
    1.46    \begin{supertabular}{rcl}
    1.47      @{syntax_def ident} & = & @{text "letter quasiletter\<^sup>*"} \\
    1.48      @{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\
    1.49 @@ -126,7 +133,7 @@
    1.50            &   & @{verbatim "\<Lambda>"}@{text "  |  "}@{verbatim "\<Xi>"}@{text "  |  "}@{verbatim "\<Pi>"}@{text "  |  "}@{verbatim "\<Sigma>"}@{text "  |"} \\
    1.51            &   & @{verbatim "\<Upsilon>"}@{text "  |  "}@{verbatim "\<Phi>"}@{text "  |  "}@{verbatim "\<Psi>"}@{text "  |  "}@{verbatim "\<Omega>"} \\
    1.52    \end{supertabular}
    1.53 -  \medskip
    1.54 +  \end{center}
    1.55  
    1.56    The syntax of @{syntax string} admits any characters, including
    1.57    newlines; ``@{verbatim "\""}'' (double-quote) and ``@{verbatim