--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Oct 07 21:28:24 2014 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Tue Oct 07 21:29:59 2014 +0200
@@ -2,9 +2,9 @@
imports Base Main
begin
-chapter {* Inner syntax --- the term language \label{ch:inner-syntax} *}
+chapter \<open>Inner syntax --- the term language \label{ch:inner-syntax}\<close>
-text {* The inner syntax of Isabelle provides concrete notation for
+text \<open>The inner syntax of Isabelle provides concrete notation for
the main entities of the logical framework, notably @{text
"\<lambda>"}-terms with types and type classes. Applications may either
extend existing syntactic categories by additional notation, or
@@ -25,14 +25,14 @@
distinction of lexical language versus context-free grammar (see
\secref{sec:pure-syntax}), and various mechanisms for \emph{syntax
transformations} (see \secref{sec:syntax-transformations}).
-*}
+\<close>
-section {* Printing logical entities *}
+section \<open>Printing logical entities\<close>
-subsection {* Diagnostic commands \label{sec:print-diag} *}
+subsection \<open>Diagnostic commands \label{sec:print-diag}\<close>
-text {*
+text \<open>
\begin{matharray}{rcl}
@{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -115,12 +115,12 @@
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
systematic way to include formal items into the printed text
document.
-*}
+\<close>
-subsection {* Details of printed content *}
+subsection \<open>Details of printed content\<close>
-text {*
+text \<open>
\begin{tabular}{rcll}
@{attribute_def show_markup} & : & @{text attribute} \\
@{attribute_def show_types} & : & @{text attribute} & default @{text false} \\
@@ -241,12 +241,12 @@
relevant for user interfaces).
\end{description}
-*}
+\<close>
-subsection {* Alternative print modes \label{sec:print-modes} *}
+subsection \<open>Alternative print modes \label{sec:print-modes}\<close>
-text {*
+text \<open>
\begin{mldecls}
@{index_ML print_mode_value: "unit -> string list"} \\
@{index_ML Print_Mode.with_modes: "string list -> ('a -> 'b) -> 'a -> 'b"} \\
@@ -312,12 +312,12 @@
alternative output notation.
\end{itemize}
-*}
+\<close>
-section {* Mixfix annotations \label{sec:mixfix} *}
+section \<open>Mixfix annotations \label{sec:mixfix}\<close>
-text {* Mixfix annotations specify concrete \emph{inner syntax} of
+text \<open>Mixfix annotations specify concrete \emph{inner syntax} of
Isabelle types and terms. Locally fixed parameters in toplevel
theorem statements, locale and class specifications also admit
mixfix annotations in a fairly uniform manner. A mixfix annotation
@@ -352,12 +352,12 @@
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. *}
+ ``@{verbatim "++"}'' for an infix symbol.\<close>
-subsection {* The general mixfix form *}
+subsection \<open>The general mixfix form\<close>
-text {* In full generality, mixfix declarations work as follows.
+text \<open>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
@@ -436,12 +436,12 @@
The general idea of pretty printing with blocks and breaks is also
described in @{cite "paulson-ml2"}; it goes back to @{cite "Oppen:1980"}.
-*}
+\<close>
-subsection {* Infixes *}
+subsection \<open>Infixes\<close>
-text {* Infix operators are specified by convenient short forms that
+text \<open>Infix operators are specified by convenient short forms that
abbreviate general mixfix annotations as follows:
\begin{center}
@@ -468,12 +468,12 @@
The alternative notation @{verbatim "op"}~@{text sy} is introduced
in addition. Thus any infix operator may be written in prefix form
(as in ML), independently of the number of arguments in the term.
-*}
+\<close>
-subsection {* Binders *}
+subsection \<open>Binders\<close>
-text {* A \emph{binder} is a variable-binding construct such as a
+text \<open>A \emph{binder} is a variable-binding construct such as a
quantifier. The idea to formalize @{text "\<forall>x. b"} as @{text "All
(\<lambda>x. b)"} for @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow> bool"} already goes back
to @{cite church40}. Isabelle declarations of certain higher-order
@@ -509,12 +509,12 @@
Furthermore, a syntax translation to transforms @{text "c_binder x\<^sub>1
\<dots> x\<^sub>n b"} into iterated application @{text "c (\<lambda>x\<^sub>1. \<dots> c (\<lambda>x\<^sub>n. b)\<dots>)"}.
- This works in both directions, for parsing and printing. *}
+ This works in both directions, for parsing and printing.\<close>
-section {* Explicit notation \label{sec:notation} *}
+section \<open>Explicit notation \label{sec:notation}\<close>
-text {*
+text \<open>
\begin{matharray}{rcll}
@{command_def "type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "no_type_notation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@@ -562,14 +562,14 @@
works within an Isar proof body.
\end{description}
-*}
+\<close>
-section {* The Pure syntax \label{sec:pure-syntax} *}
+section \<open>The Pure syntax \label{sec:pure-syntax}\<close>
-subsection {* Lexical matters \label{sec:inner-lex} *}
+subsection \<open>Lexical matters \label{sec:inner-lex}\<close>
-text {* The inner lexical syntax vaguely resembles the outer one
+text \<open>The inner lexical syntax vaguely resembles the outer one
(\secref{sec:outer-lex}), but some details are different. There are
two main categories of inner syntax tokens:
@@ -617,12 +617,12 @@
The derived categories @{syntax_def (inner) num_const}, and @{syntax_def
(inner) float_const}, provide robust access to the respective tokens: the
syntax tree holds a syntactic constant instead of a free variable.
-*}
+\<close>
-subsection {* Priority grammars \label{sec:priority-grammar} *}
+subsection \<open>Priority grammars \label{sec:priority-grammar}\<close>
-text {* A context-free grammar consists of a set of \emph{terminal
+text \<open>A context-free grammar consists of a set of \emph{terminal
symbols}, a set of \emph{nonterminal symbols} and a set of
\emph{productions}. Productions have the form @{text "A = \<gamma>"},
where @{text A} is a nonterminal and @{text \<gamma>} is a string of
@@ -692,12 +692,12 @@
& @{text "|"} & @{verbatim "-"} @{text "A\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
\end{tabular}
\end{center}
-*}
+\<close>
-subsection {* The Pure grammar \label{sec:pure-grammar} *}
+subsection \<open>The Pure grammar \label{sec:pure-grammar}\<close>
-text {* The priority grammar of the @{text "Pure"} theory is defined
+text \<open>The priority grammar of the @{text "Pure"} theory is defined
approximately like this:
\begin{center}
@@ -896,12 +896,12 @@
translation rules (\secref{sec:syn-trans}), notably on the LHS.
\end{itemize}
-*}
+\<close>
-subsection {* Inspecting the syntax *}
+subsection \<open>Inspecting the syntax\<close>
-text {*
+text \<open>
\begin{matharray}{rcl}
@{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
@@ -956,12 +956,12 @@
\end{description}
\end{description}
-*}
+\<close>
-subsection {* Ambiguity of parsed expressions *}
+subsection \<open>Ambiguity of parsed expressions\<close>
-text {*
+text \<open>
\begin{tabular}{rcll}
@{attribute_def syntax_ambiguity_warning} & : & @{text attribute} & default @{text true} \\
@{attribute_def syntax_ambiguity_limit} & : & @{text attribute} & default @{text 10} \\
@@ -991,12 +991,12 @@
in case of an ambiguity.
\end{description}
-*}
+\<close>
-section {* Syntax transformations \label{sec:syntax-transformations} *}
+section \<open>Syntax transformations \label{sec:syntax-transformations}\<close>
-text {* The inner syntax engine of Isabelle provides separate
+text \<open>The inner syntax engine of Isabelle provides separate
mechanisms to transform parse trees either via rewrite systems on
first-order ASTs (\secref{sec:syn-trans}), or ML functions on ASTs
or syntactic @{text "\<lambda>"}-terms (\secref{sec:tr-funs}). This works
@@ -1042,12 +1042,12 @@
or constants needs to be implemented as syntax transformation (see
below). Anything else is better done via check/uncheck: a prominent
example application is the @{command abbreviation} concept of
- Isabelle/Pure. *}
+ Isabelle/Pure.\<close>
-subsection {* Abstract syntax trees \label{sec:ast} *}
+subsection \<open>Abstract syntax trees \label{sec:ast}\<close>
-text {* The ML datatype @{ML_type Ast.ast} explicitly represents the
+text \<open>The ML datatype @{ML_type Ast.ast} explicitly represents the
intermediate AST format that is used for syntax rewriting
(\secref{sec:syn-trans}). It is defined in ML as follows:
\begin{ttbox}
@@ -1081,12 +1081,12 @@
where @{verbatim "(\"_abs\" x t)"} becomes an @{ML Abs} node and
occurrences of @{verbatim x} in @{verbatim t} are replaced by bound
variables (represented as de-Bruijn indices).
-*}
+\<close>
-subsubsection {* AST constants versus variables *}
+subsubsection \<open>AST constants versus variables\<close>
-text {* Depending on the situation --- input syntax, output syntax,
+text \<open>Depending on the situation --- input syntax, output syntax,
translation patterns --- the distinction of atomic ASTs as @{ML
Ast.Constant} versus @{ML Ast.Variable} serves slightly different
purposes.
@@ -1121,12 +1121,12 @@
corresponds to an AST application of some constant for @{text foo}
and variable arguments for @{text "'a"} and @{text "'b"}. Note that
the postfix application is merely a feature of the concrete syntax,
- while in the AST the constructor occurs in head position. *}
+ while in the AST the constructor occurs in head position.\<close>
-subsubsection {* Authentic syntax names *}
+subsubsection \<open>Authentic syntax names\<close>
-text {* Naming constant entities within ASTs is another delicate
+text \<open>Naming constant entities within ASTs is another delicate
issue. Unqualified names are resolved in the name space tables in
the last stage of parsing, after all translations have been applied.
Since syntax transformations do not know about this later name
@@ -1160,12 +1160,12 @@
In other words, syntax transformations that operate on input terms
written as prefix applications are difficult to make robust.
Luckily, this case rarely occurs in practice, because syntax forms
- to be translated usually correspond to some concrete notation. *}
+ to be translated usually correspond to some concrete notation.\<close>
-subsection {* Raw syntax and translations \label{sec:syn-trans} *}
+subsection \<open>Raw syntax and translations \label{sec:syn-trans}\<close>
-text {*
+text \<open>
\begin{tabular}{rcll}
@{command_def "nonterminal"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "syntax"} & : & @{text "theory \<rightarrow> theory"} \\
@@ -1337,11 +1337,11 @@
List} in Isabelle/HOL.
\end{itemize}
-*}
+\<close>
-subsubsection {* Applying translation rules *}
+subsubsection \<open>Applying translation rules\<close>
-text {* As a term is being parsed or printed, an AST is generated as
+text \<open>As a term is being parsed or printed, an AST is generated as
an intermediate form according to \figref{fig:parse-print}. The AST
is normalized by applying translation rules in the manner of a
first-order term rewriting system. We first examine how a single
@@ -1410,12 +1410,12 @@
functions (see also \secref{sec:tr-funs}), which is in fact the same
mechanism used in built-in @{keyword "binder"} declarations.
\end{warn}
-*}
+\<close>
-subsection {* Syntax translation functions \label{sec:tr-funs} *}
+subsection \<open>Syntax translation functions \label{sec:tr-funs}\<close>
-text {*
+text \<open>
\begin{matharray}{rcl}
@{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\
@@ -1492,12 +1492,12 @@
names occurring in parse trees (unqualified constants etc.).
\end{description}
-*}
+\<close>
-subsubsection {* The translation strategy *}
+subsubsection \<open>The translation strategy\<close>
-text {* The different kinds of translation functions are invoked during
+text \<open>The different kinds of translation functions are invoked during
the transformations between parse trees, ASTs and syntactic terms
(cf.\ \figref{fig:parse-print}). Whenever a combination of the form
@{text "c x\<^sub>1 \<dots> x\<^sub>n"} is encountered, and a translation function
@@ -1545,20 +1545,20 @@
the status of constant versus variable is not yet know during
parsing. This is in contrast to print translations, where constants
are explicitly known from the given term in its fully internal form.
-*}
+\<close>
-subsection {* Built-in syntax transformations *}
+subsection \<open>Built-in syntax transformations\<close>
-text {*
+text \<open>
Here are some further details of the main syntax transformation
phases of \figref{fig:parse-print}.
-*}
+\<close>
-subsubsection {* Transforming parse trees to ASTs *}
+subsubsection \<open>Transforming parse trees to ASTs\<close>
-text {* The parse tree is the raw output of the parser. It is
+text \<open>The parse tree is the raw output of the parser. It is
transformed into an AST according to some basic scheme that may be
augmented by AST translation functions as explained in
\secref{sec:tr-funs}.
@@ -1598,12 +1598,12 @@
translations need to be ready to cope with them. The built-in
syntax transformation from parse trees to ASTs insert additional
constraints that represent source positions.
-*}
+\<close>
-subsubsection {* Transforming ASTs to terms *}
+subsubsection \<open>Transforming ASTs to terms\<close>
-text {* After application of macros (\secref{sec:syn-trans}), the AST
+text \<open>After application of macros (\secref{sec:syn-trans}), the AST
is transformed into a term. This term still lacks proper type
information, but it might contain some constraints consisting of
applications with head @{verbatim "_constrain"}, where the second
@@ -1620,12 +1620,12 @@
bound variables are introduced by parse translations associated with
certain syntax constants. Thus @{verbatim "(_abs x x)"} eventually
becomes a de-Bruijn term @{verbatim "Abs (\"x\", _, Bound 0)"}.
-*}
+\<close>
-subsubsection {* Printing of terms *}
+subsubsection \<open>Printing of terms\<close>
-text {* The output phase is essentially the inverse of the input
+text \<open>The output phase is essentially the inverse of the input
phase. Terms are translated via abstract syntax trees into
pretty-printed text.
@@ -1672,6 +1672,6 @@
\medskip White space is \emph{not} inserted automatically. If
blanks (or breaks) are required to separate tokens, they need to be
specified in the mixfix declaration (\secref{sec:mixfix}).
-*}
+\<close>
end