--- a/doc-src/IsarRef/syntax.tex Tue Aug 24 11:54:13 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex Tue Aug 24 15:38:18 1999 +0200
@@ -1,10 +1,9 @@
-\chapter{Isar document syntax}
+\chapter{Isar Document Syntax}
We give a complete reference of all basic syntactic entities underlying the
-the Isabelle/Isar document syntax. This chapter will not introduce any actual
-theory and proof commands, though (cf.\ chapter~\ref{ch:pure-syntax} and
-later).
+Isabelle/Isar document syntax. Actual theory and proof commands will be
+introduced later on.
\medskip
@@ -17,10 +16,10 @@
are legal term specifications, while \texttt{x + y} is not.
\begin{warn}
- Note that old-style Isabelle theories used to fake parts of the inner type
- syntax, with complicated rules when quotes may be omitted. Despite the
- minor drawback of requiring quotes more often, Isabelle/Isar is simpler and
- more robust in that respect.
+ Note that Isabelle theories used to fake parts of the inner type syntax,
+ with complicated rules when quotes may be omitted. Despite the minor
+ drawback of requiring quotes more often, Isabelle/Isar is simpler and more
+ robust in that respect.
\end{warn}
@@ -31,6 +30,7 @@
as given in \cite{isabelle-ref}. These different levels of syntax should not
be confused, though.
+%FIXME keyword, command
\begin{matharray}{rcl}
ident & = & letter~quasiletter^* \\
longident & = & ident\verb,.,ident~\dots~ident \\
@@ -58,22 +58,22 @@
ML-style control character notation is not supported. The body of
\texttt{verbatim} may consist of any text not containing \verb|*}|.
-Comments take the form \texttt{(*~\dots~*)} and may be nested, just as in ML.
-Note that these are \emph{source} comments only, which are stripped after
-lexical analysis of the input. The Isar document syntax also provides several
+Comments take the form \texttt{(*~\dots~*)} and may be nested, just as in
+ML.\footnote{Proof~General may get confused by nested comments, though.} Note
+that these are \emph{source} comments only, which are stripped after lexical
+analysis of the input. The Isar document syntax also provides several
elements of \emph{formal comments} that are actually part of the text (see
\S\ref{sec:comments}, \S\ref{sec:formal-cmt-thy}, \S\ref{sec:formal-cmt-prf}).
\section{Common syntax entities}
-The Isar proof and theory language syntax has been carefully designed with
-orthogonality in mind. Subsequently, we introduce several basic syntactic
-entities, such as names, terms, theorem specifications, which have been
-factored out of the actual Isar language elements described later.
+Subsequently, we introduce several basic syntactic entities, such as names,
+terms, theorem specifications, which have been factored out of the actual Isar
+language elements to be described later.
Note that some of the basic syntactic entities introduced below act much like
-tokens rather than nonterminals, in particular for the sake of error messages.
+tokens rather than nonterminals, especially for the sake of error messages.
E.g.\ syntax elements such as $\CONSTS$ referring to \railqtoken{name} or
\railqtoken{type} would really report a missing name or type rather than any
of the constituent primitive tokens such as \railtoken{ident} or
@@ -108,12 +108,12 @@
are admitted as well. Almost any of the Isar commands may be annotated by
some marginal \railnonterm{comment} of the form \texttt{--} \railqtoken{text}.
Note that this kind of comment is actually part of the language, while source
-level comments \verb|(*|\dots\verb|*)| are already stripped at the lexical
-level. A few commands such as $\PROOFNAME$ admit additional markup with a
-``level of interest'': \texttt{\%} followed by an optional number $n$ (default
-$n = 1$) indicates that the respective part of the document becomes $n$ levels
-more obscure; \texttt{\%\%} means that interest drops by $\infty$ ---
-\emph{abandon every hope, who enter here}.
+level comments \verb|(*|\dots\verb|*)| are stripped at the lexical level. A
+few commands such as $\PROOFNAME$ admit additional markup with a ``level of
+interest'': \texttt{\%} followed by an optional number $n$ (default $n = 1$)
+indicates that the respective part of the document becomes $n$ levels more
+obscure; \texttt{\%\%} means that interest drops by $\infty$ --- abandon every
+hope, who enter here.
\indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
\begin{rail}
@@ -126,10 +126,10 @@
\end{rail}
-\subsection{Type classes, Sorts and arities}
+\subsection{Type classes, sorts and arities}
The syntax of sorts and arities is given directly at the outer level. Note
-that this is in contrast to that types and terms (see \ref{sec:types-terms}).
+that this is in contrast to types and terms (see \ref{sec:types-terms}).
\indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
\indexouternonterm{classdecl}
@@ -148,12 +148,12 @@
\subsection{Types and terms}\label{sec:types-terms}
The actual inner Isabelle syntax, that of types and terms of the logic, is far
-too flexible in order to be modelled explicitly at the outer theory level.
-Basically, any such entity has to be quoted at the outer level to turn it into
-a single token (the parsing and type-checking is performed later). For
-convenience, a slightly more liberal convention is adopted: quotes may be
-omitted for any type or term that is already \emph{atomic at the outer level}.
-E.g.\ one may write just \texttt{x} instead of \texttt{"x"}.
+too advanced in order to be modelled explicitly at the outer theory level.
+Basically, any such entity has to be quoted here to turn it into a single
+token (the parsing and type-checking is performed later). For convenience, a
+slightly more liberal convention is adopted: quotes may be omitted for any
+type or term that is already \emph{atomic} at the outer level. E.g.\ one may
+write just \texttt{x} instead of \texttt{"x"}.
\indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
\begin{rail}
@@ -215,12 +215,12 @@
\subsection{Attributes and theorems}\label{sec:syn-att}
Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their own
-``semi-inner'' syntax, in the sense that input conforming \railnonterm{args}
-below are parsed by the attribute a second time. The attribute argument
-specifications may be any sequence of atomic entities (identifiers, strings
-etc.), or properly bracketed argument lists. Below \railqtoken{atom} refers
-to any atomic entity, including \railtoken{keyword}s conforming to
-\railtoken{symident}.
+``semi-inner'' syntax, in the sense that input conforming to
+\railnonterm{args} below is parsed by the attribute a second time. The
+attribute argument specifications may be any sequence of atomic entities
+(identifiers, strings etc.), or properly bracketed argument lists. Below
+\railqtoken{atom} refers to any atomic entity, including \railtoken{keyword}s
+conforming to \railtoken{symident}.
\indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
\begin{rail}
@@ -240,7 +240,7 @@
Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs}
(the former requires an actual singleton result). Any of these theorem
specifications may include lists of attributes both on the left and right hand
-sides; attributes are applied to the any immediately preceding theorem.
+sides; attributes are applied to any immediately preceding theorem.
\indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
@@ -267,10 +267,10 @@
``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
``\texttt{?}'' (try), ``\texttt{*}'' (repeat ${} \ge 0$ times), ``\texttt{+}''
(repeat ${} > 0$ times). In practice, proof methods are usually just a comma
-separated list of (\railqtoken{nameref}~\railnonterm{args}) specifications.
+separated list of \railqtoken{nameref}~\railnonterm{args} specifications.
Thus the syntax is similar to that of attributes, with plain parentheses
-instead of square brackets (see also \S\ref{sec:syn-att}). Note that
-parentheses may be dropped for single method specifications without arguments.
+instead of square brackets. Note that parentheses may be dropped for single
+method specifications without arguments.
\indexouternonterm{method}
\begin{rail}