--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Thu Nov 13 21:45:40 2008 +0100
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Thu Nov 13 21:48:19 2008 +0100
@@ -307,117 +307,6 @@
*}
-subsection {* Mixfix annotations *}
-
-text {*
- Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
- types and terms. Some commands such as @{command "types"} (see
- \secref{sec:types-pure}) admit infixes only, while @{command
- "consts"} (see \secref{sec:consts}) and @{command "syntax"} (see
- \secref{sec:syn-trans}) support the full range of general mixfixes
- and binders.
-
- \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
- \begin{rail}
- infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')'
- ;
- mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
- ;
- structmixfix: mixfix | '(' 'structure' ')'
- ;
-
- prios: '[' (nat + ',') ']'
- ;
- \end{rail}
-
- Here the \railtok{string} specifications refer to the actual mixfix
- template, which may include literal text, spacing, blocks, and
- arguments (denoted by ``@{text _}''); the special symbol
- ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') represents an index
- argument that specifies an implicit structure reference (see also
- \secref{sec:locale}). Infix and binder declarations provide common
- abbreviations for particular mixfix declarations. So in practice,
- mixfix templates mostly degenerate to literal text for concrete
- syntax, such as ``@{verbatim "++"}'' for an infix symbol.
-
- \medskip In full generality, mixfix declarations work as follows.
- Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is
- annotated by @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text
- "mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of
- delimiters that surround argument positions as indicated by
- underscores.
-
- Altogether this determines a production for a context-free priority
- grammar, where for each argument @{text "i"} the syntactic category
- is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and
- the result category is determined from @{text "\<tau>"} (with
- priority @{text "p"}). Priority specifications are optional, with
- default 0 for arguments and 1000 for the result.
-
- Since @{text "\<tau>"} may be again a function type, the constant
- type scheme may have more argument positions than the mixfix
- pattern. Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for
- @{text "m > n"} works by attaching concrete notation only to the
- innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"}
- instead. If a term has fewer arguments than specified in the mixfix
- template, the concrete syntax is ignored.
-
- \medskip A mixfix template may also contain additional directives
- for pretty printing, notably spaces, blocks, and breaks. The
- general template format is a sequence over any of the following
- entities.
-
- \begin{itemize}
-
- \item @{text "\<^bold>d"} is a delimiter, namely a non-empty
- sequence of characters other than the special characters @{text "'"}
- (single quote), @{text "_"} (underscore), @{text "\<index>"} (index
- symbol), @{text "/"} (slash), @{text "("} and @{text ")"}
- (parentheses).
-
- A single quote escapes the special meaning of these meta-characters,
- producing a literal version of the following character, unless that
- is a blank. A single quote followed by a blank separates
- delimiters, without affecting printing, but input tokens may have
- additional white space here.
-
- \item @{text "_"} is an argument position, which stands for a
- certain syntactic category in the underlying grammar.
-
- \item @{text "\<index>"} is an indexed argument position; this is
- the place where implicit structure arguments can be attached.
-
- \item @{text "\<^bold>s"} is a non-empty sequence of spaces for
- printing. This and the following specifications do not affect
- parsing at all.
-
- \item @{text "(\<^bold>n"} opens a pretty printing block. The
- optional number specifies how much indentation to add when a line
- break occurs within the block. If the parenthesis is not followed
- by digits, the indentation defaults to 0. A block specified via
- @{text "(00"} is unbreakable.
-
- \item @{text ")"} closes a pretty printing block.
-
- \item @{text "//"} forces a line break.
-
- \item @{text "/\<^bold>s"} allows a line break. Here @{text
- "\<^bold>s"} stands for the string of spaces (zero or more) right
- after the slash. These spaces are printed if the break is
- \emph{not} taken.
-
- \end{itemize}
-
- For example, the template @{text "(_ +/ _)"} specifies an infix
- operator. There are two argument positions; the delimiter @{text
- "+"} is preceded by a space and followed by a space or line break;
- the entire phrase is a pretty printing block.
-
- The general idea of pretty printing with blocks and breaks is also
- described in \cite{paulson-ml2}.
-*}
-
-
subsection {* Attributes and theorems \label{sec:syn-att} *}
text {* Attributes have their own ``semi-inner'' syntax, in the sense