theory Readme
imports Base
begin

chapter \<open>Comments for Authors\<close>

text \<open>

  \begin{itemize}
  \item This tutorial can be compiled on the command-line with:

  @{text [display] "$ isabelle build -c -v -d . Cookbook"}

  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 & \<open>\ichcite{\<dots>}\<close> & \<open>\isccite{\<dots>}\<close>\\
  Isar Reference Manual & \<open>\rchcite{\<dots>}\<close> & \<open>\rsccite{\<dots>}\<close>\\
  \end{tabular}
  \end{center}

  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 
  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$] \<open>@{ML \<open>expr\<close> 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 \<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}
  \<open>@{ML \<open>1 + 3\<close>}\<close>         &                 & @{ML \<open>1 + 3\<close>}\\
  \<open>@{ML \<open>a + b\<close> for a b}\<close> & \;\;produce\;\; & @{ML \<open>a + b\<close> for a b}\\
  \<open>@{ML explode in Symbol}\<close> &                 & @{ML explode in Symbol}\\
  \end{tabular}
  \end{center}

  \item[$\bullet$] \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> should be used to
  display ML-expressions and their response.  The first expression is checked
  like in the antiquotation \<open>@{ML \<open>expr\<close>}\<close>; the second is a pattern
  that specifies the result the first expression produces. This pattern can
  contain @{text [quotes] "_"} (which will be printed as @{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}
  \<open>@{ML_matchresult \<open>1+2\<close> \<open>3\<close>}\<close>\\
  \<open>@{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,_)\<close>}\<close>
  \end{tabular}
  \end{center}

  which produce respectively

  \begin{center}\small
  \begin{tabular}{p{3cm}p{3cm}}
  @{ML_matchresult \<open>1+2\<close> \<open>3\<close>} &  
  @{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,_)\<close>}
  \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$] \<open>@{ML_matchresult_fake \<open>expr\<close> \<open>pat\<close>}\<close> works just
  like the antiquotation \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<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}
  \<open>@{ML_matchresult_fake\<close> & \<open>\<open>term_of @{theory} @{term "a + b = c"}\<close>\<close>\\
                               & \<open>\<open>a + b = c\<close>}\<close>\smallskip\\ 
  \<open>@{ML_matchresult_fake\<close> & \<open>\<open>($$ "x") (explode "world")\<close>\<close>\\ 
                               & \<open>\<open>Exception FAIL raised\<close>}\<close>
  \end{tabular}
  \end{center}

  which produce respectively

  \begin{center}\small
  \begin{tabular}{p{7.2cm}}
  @{ML_matchresult_fake \<open>Thm.cterm_of @{context} @{term "a + b = c"}\<close> \<open>a + b = c\<close>}\smallskip\\
  @{ML_matchresult_fake \<open>($$ "x") (Symbol.explode "world")\<close> \<open>Exception FAIL raised\<close>}
  \end{tabular}
  \end{center}
  
  This output mimics to some extend what the user sees when running the
  code.

  \item[$\bullet$] \<open>@{ML_matchresult_fake_both \<open>expr\<close> \<open>pat\<close>}\<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}
  \<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm "1 + True"}"\<close>\\
                                    & \<open>"Type unification failed \<dots>"}\<close>
  \end{tabular}
  \end{center}

  \item[$\bullet$] \<open>@{ML_response \<open>expr\<close>}\<close> can be
  used to show the expression and the corresponding output. An example is:

  \begin{center}\small
  \begin{tabular}{ll}
  \<open>@{ML_response\<close> & \<open>\<open>1 upto 10\<close>}\<close>
  \end{tabular}
  \end{center}

 which produces

  \begin{center}\small
  @{ML_response \<open>1 upto 10\<close>}
  \end{center}
 
  You can give a second argument for the expected response. This is matched against the actual
  response by crude wildcard matching where whitespace and \<open>\<dots>\<close> are treated as wildcard.

  \begin{center}\small
  \begin{tabular}{ll}
  \<open>@{ML_response\<close> & \<open>\<open>1 upto 20\<close>\<close>\\
                  & \<open>"[1, 2, 3, 4, 5, 6\<dots>\<close>\\
                  &   \<open>18, 19, 20]"}\<close>\\
  \end{tabular}
  \end{center}

  will produce

  @{ML_response \<open>1 upto 20\<close>
\<open>[1, 2, 3, 4, 5, 6\<dots> 
  18, 19, 20]\<close>}

  Note that exceptions are also converted to strings and can thus be checked in the response 
  string.

  @{ML_response \<open>error "hallo"\<close>
  \<open>hallo\<close>}

So as a rule of thumb, to facilitate result checking use prefer this order:
\begin{enumerate}
 \item \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close>    
 \item \<open>@{ML_response \<open>expr\<close> \<open>string\<close>}\<close>
 \item \<open>@{ML_matchresult_fake \<open>expr\<close> \<open>pat\<close>}\<close> or \<open>@{ML_response \<open>expr\<close>}\<close>
 \item \<open>@{ML_matchresult_fake_both \<open>expr\<close> \<open>pat\<close>}\<close>
\end{enumerate}

  \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] \<open>@{ML_file "Pure/General/basics.ML"}\<close>}
  \end{itemize}

  The listed antiquotations honour options including \<open>[display]\<close> and 
  \<open>[gray]\<close>. For example

  
  \item Functions and value bindings cannot be defined inside antiquotations; they need
  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}~\<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>



end