theory Readme+ −
imports Base+ −
begin+ −
+ −
chapter {* Comments for Authors *}+ −
+ −
text {*+ −
+ −
\begin{itemize}+ −
\item This tutorial can be compiled on the command-line with:+ −
+ −
@{text [display] "$ isabelle make"}+ −
+ −
You very likely need a recent snapshot of Isabelle in order to compile+ −
the tutorial. Some parts of the tutorial also rely on compilation with+ −
PolyML.+ −
+ −
\item You can include references to other Isabelle manuals using the + −
reference names from those manuals. To do this the following+ −
four \LaTeX{} commands are defined:+ −
+ −
\begin{center}+ −
\begin{tabular}{l|c|c}+ −
& Chapters & Sections\\\hline+ −
Implementation Manual & @{text "\\ichcite{\<dots>}"} & @{text "\\isccite{\<dots>}"}\\+ −
Isar Reference Manual & @{text "\\rchcite{\<dots>}"} & @{text "\\rsccite{\<dots>}"}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic + −
in the implementation manual, namely \ichcite{ch:logic}.+ −
+ −
\item There are various document antiquotations defined for the + −
tutorial. They allow to check the written text against the current+ −
Isabelle code and also allow to show responses of the ML-compiler.+ −
Therefore authors are strongly encouraged to use antiquotations wherever+ −
appropriate.+ −
+ −
The following antiquotations are defined:+ −
+ −
\begin{itemize}+ −
\item[$\bullet$] @{text "@{ML \"expr\" for vars in structs}"} should be used+ −
for displaying any ML-ex\-pression, because the antiquotation checks whether+ −
the expression is valid ML-code. The @{text "for"}- and @{text+ −
"in"}-arguments are optional. The former is used for evaluating open+ −
expressions by giving a list of free variables. The latter is used to+ −
indicate in which structure or structures the ML-expression should be+ −
evaluated. Examples are:+ −
+ −
\begin{center}\small+ −
\begin{tabular}{lll}+ −
@{text "@{ML \"1 + 3\"}"} & & @{ML "1 + 3"}\\+ −
@{text "@{ML \"a + b\" for a b}"} & \;\;produce\;\; & @{ML "a + b" for a b}\\+ −
@{text "@{ML Ident in OuterLex}"} & & @{ML Ident in OuterLex}\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to+ −
display ML-expressions and their response. The first expression is checked+ −
like in the antiquotation @{text "@{ML \"expr\"}"}; the second is a pattern+ −
that specifies the result the first expression produces. This pattern can+ −
contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the+ −
first expression will be checked against this pattern. Examples are:+ −
+ −
\begin{center}\small+ −
\begin{tabular}{l}+ −
@{text "@{ML_response \"1+2\" \"3\"}"}\\+ −
@{text "@{ML_response \"(1+2,3)\" \"(3,\<dots>)\"}"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
which produce respectively+ −
+ −
\begin{center}\small+ −
\begin{tabular}{p{3cm}p{3cm}}+ −
@{ML_response "1+2" "3"} & + −
@{ML_response "(1+2,3)" "(3,\<dots>)"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
Note that this antiquotation can only be used when the result can be+ −
constructed: it does not work when the code produces an exception or returns + −
an abstract datatype (like @{ML_type thm} or @{ML_type cterm}).+ −
+ −
\item[$\bullet$] @{text "@{ML_response_fake \"expr\" \"pat\"}"} works just+ −
like the antiquotation @{text "@{ML_response \"expr\" \"pat\"}"} above,+ −
except that the result-specification is not checked. Use this antiquotation+ −
when the result cannot be constructed or the code generates an+ −
exception. Examples are:+ −
+ −
\begin{center}\small+ −
\begin{tabular}{ll}+ −
@{text "@{ML_response_fake"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\+ −
& @{text "\"a + b = c\"}"}\smallskip\\ + −
@{text "@{ML_response_fake"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\ + −
& @{text "\"Exception FAIL raised\"}"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
which produce respectively+ −
+ −
\begin{center}\small+ −
\begin{tabular}{p{7.2cm}}+ −
@{ML_response_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\+ −
@{ML_response_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
This output mimics to some extend what the user sees when running the+ −
code.+ −
+ −
\item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be+ −
used to show erroneous code. Neither the code nor the response will be+ −
checked. An example is:+ −
+ −
\begin{center}\small+ −
\begin{tabular}{ll}+ −
@{text "@{ML_response_fake_both"} & @{text "\"@{cterm \\\"1 + True\\\"}\""}\\+ −
& @{text "\"Type unification failed \<dots>\"}"}+ −
\end{tabular}+ −
\end{center}+ −
+ −
\item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when+ −
referring to a file. It checks whether the file exists. An example+ −
is + −
+ −
@{text [display] "@{ML_file \"Pure/General/basics.ML\"}"}+ −
\end{itemize}+ −
+ −
The listed antiquotations honour options including @{text "[display]"} and + −
@{text "[quotes]"}. For example+ −
+ −
\begin{center}\small+ −
@{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"}+ −
\end{center}+ −
+ −
whereas+ −
+ −
\begin{center}\small+ −
@{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"}+ −
\end{center}+ −
+ −
\item Functions and value bindings cannot be defined inside antiquotations; they need+ −
to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}+ −
environments. In this way they are also checked by the compiler. Some \LaTeX-hack in + −
the tutorial, however, ensures that the environment markers are not printed.+ −
+ −
\item Line numbers can be printed using + −
\isacommand{ML} \isa{\%linenos}~@{text "\<verbopen> \<dots> \<verbclose>"}+ −
for ML-code or \isacommand{lemma} \isa{\%linenos} @{text "..."} for proofs. The+ −
tag is \isa{\%linenosgray} when the numbered text should be gray. + −
+ −
\end{itemize}+ −
+ −
*}+ −
+ −
+ −
+ −
end+ −