--- a/ProgTutorial/Readme.thy Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Readme.thy Tue May 14 17:10:47 2019 +0200
@@ -2,9 +2,9 @@
imports Base
begin
-chapter {* Comments for Authors *}
+chapter \<open>Comments for Authors\<close>
-text {*
+text \<open>
\begin{itemize}
\item This tutorial can be compiled on the command-line with:
@@ -22,12 +22,12 @@
\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>}"}\\
+ Implementation Manual & \<open>\ichcite{\<dots>}\<close> & \<open>\isccite{\<dots>}\<close>\\
+ Isar Reference Manual & \<open>\rchcite{\<dots>}\<close> & \<open>\rsccite{\<dots>}\<close>\\
\end{tabular}
\end{center}
- So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic
+ So \<open>\ichcite{ch:logic}\<close> 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
@@ -39,33 +39,32 @@
The following antiquotations are defined:
\begin{itemize}
- \item[$\bullet$] @{text "@{ML \"expr\" for vars in structs}"} should be used
+ \item[$\bullet$] \<open>@{ML "expr" for vars in structs}\<close> 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
+ the expression is valid ML-code. The \<open>for\<close>- and \<open>in\<close>-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}\\
+ \<open>@{ML "1 + 3"}\<close> & & @{ML "1 + 3"}\\
+ \<open>@{ML "a + b" for a b}\<close> & \;\;produce\;\; & @{ML "a + b" for a b}\\
+ \<open>@{ML Ident in OuterLex}\<close> & & @{ML Ident in OuterLex}\\
\end{tabular}
\end{center}
- \item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to
+ \item[$\bullet$] \<open>@{ML_response "expr" "pat"}\<close> 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
+ like in the antiquotation \<open>@{ML "expr"}\<close>; 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>)\"}"}
+ \<open>@{ML_response "1+2" "3"}\<close>\\
+ \<open>@{ML_response "(1+2,3)" "(3,\<dots>)"}\<close>
\end{tabular}
\end{center}
@@ -82,18 +81,18 @@
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,
+ \item[$\bullet$] \<open>@{ML_response_fake "expr" "pat"}\<close> works just
+ like the antiquotation \<open>@{ML_response "expr" "pat"}\<close> 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\"}"}
+ \<open>@{ML_response_fake\<close> & \<open>"cterm_of @{theory} @{term \"a + b = c\"}"}\<close>\\
+ & \<open>"a + b = c"}\<close>\smallskip\\
+ \<open>@{ML_response_fake\<close> & \<open>"($$ \"x\") (explode \"world\")"\<close>\\
+ & \<open>"Exception FAIL raised"}\<close>
\end{tabular}
\end{center}
@@ -109,50 +108,50 @@
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
+ \item[$\bullet$] \<open>@{ML_response_fake_both "expr" "pat"}\<close> 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>\"}"}
+ \<open>@{ML_response_fake_both\<close> & \<open>"@{cterm \"1 + True\"}"\<close>\\
+ & \<open>"Type unification failed \<dots>"}\<close>
\end{tabular}
\end{center}
- \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when
+ \item[$\bullet$] \<open>@{ML_file "name"}\<close> 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
+ The listed antiquotations honour options including \<open>[display]\<close> and
+ \<open>[quotes]\<close>. For example
\begin{center}\small
- @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"}
+ \<open>@{ML [quotes] "\"foo\" ^ \"bar\""}\<close> \;\;produces\;\; @{text [quotes] "foobar"}
\end{center}
whereas
\begin{center}\small
- @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"}
+ \<open>@{ML "\"foo\" ^ \"bar\""}\<close> \;\;produces only\;\; \<open>foobar\<close>
\end{center}
\item Functions and value bindings cannot be defined inside antiquotations; they need
- to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}
+ to be included inside \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close>
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
+ \isacommand{ML} \isa{\%linenos}~\<open>\<verbopen> \<dots> \<verbclose>\<close>
+ for ML-code or \isacommand{lemma} \isa{\%linenos} \<open>...\<close> for proofs. The
tag is \isa{\%linenosgray} when the numbered text should be gray.
\end{itemize}
-*}
+\<close>