1.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 22:00:12 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 22:00:39 2008 +0100
     1.3 @@ -391,7 +391,7 @@
     1.4  
     1.5  section {* The Pure syntax *}
     1.6  
     1.7 -subsection {* Priority grammars *}
     1.8 +subsection {* Priority grammars \label{sec:priority-grammar} *}
     1.9  
    1.10  text {* A context-free grammar consists of a set of \emph{terminal
    1.11    symbols}, a set of \emph{nonterminal symbols} and a set of
    1.12 @@ -643,9 +643,52 @@
    1.13    \end{itemize}
    1.14  *}
    1.15  
    1.16 +
    1.17  section {* Lexical matters \label{sec:inner-lex} *}
    1.18  
    1.19 -text FIXME
    1.20 +text {* The inner lexical syntax vaguely resembles the outer one
    1.21 +  (\secref{sec:outer-lex}), but some details are different.  There are
    1.22 +  two main categories of inner syntax tokens:
    1.23 +
    1.24 +  \begin{enumerate}
    1.25 +
    1.26 +  \item \emph{delimiters} --- the literal tokens occurring in
    1.27 +  productions of the given priority grammar (cf.\
    1.28 +  \secref{sec:priority-grammar});
    1.29 +
    1.30 +  \item \emph{named tokens} --- various categories of identifiers etc.
    1.31 +
    1.32 +  \end{enumerate}
    1.33 +
    1.34 +  Delimiters override named tokens and may thus render certain
    1.35 +  identifiers inaccessible.  Sometimes the logical context admits
    1.36 +  alternative ways to refer to the same entity, potentially via
    1.37 +  qualified names.
    1.38 +
    1.39 +  \medskip The categories for named tokens are defined once and for
    1.40 +  all as follows, reusing some categories of the outer token syntax
    1.41 +  (\secref{sec:outer-lex}).
    1.42 +
    1.43 +  \begin{center}
    1.44 +  \begin{supertabular}{rcl}
    1.45 +    @{syntax_def (inner) id} & = & @{syntax_ref ident} \\
    1.46 +    @{syntax_def (inner) longid} & = & @{syntax_ref longident} \\
    1.47 +    @{syntax_def (inner) var} & = & @{syntax_ref var} \\
    1.48 +    @{syntax_def (inner) tid} & = & @{syntax_ref typefree} \\
    1.49 +    @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\
    1.50 +    @{syntax_def (inner) num} & = & @{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat} \\
    1.51 +    @{syntax_def (inner) xnum} & = & @{verbatim "#"}@{syntax_ref nat}@{text "  |  "}@{verbatim "#-"}@{syntax_ref nat} \\
    1.52 +
    1.53 +    @{syntax_def (inner) xstr} & = & @{verbatim "''"} @{text "\<dots>"} @{verbatim "''"} \\
    1.54 +  \end{supertabular}
    1.55 +  \end{center}
    1.56 +
    1.57 +  The token categories @{syntax_ref (inner) num}, @{syntax_ref (inner)
    1.58 +  xnum}, and @{syntax_ref (inner) xstr} are not used in Pure.
    1.59 +  Object-logics may implement numerals and string constants by adding
    1.60 +  appropriate syntax declarations, together with some translation
    1.61 +  functions (e.g.\ see Isabelle/HOL).
    1.62 +*}
    1.63  
    1.64  
    1.65  section {* Syntax and translations \label{sec:syn-trans} *}