diff -r a90fc1e5fb19 -r abba35b98892 doc-src/IsarRef/syntax.tex --- 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}