--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Readme.thy Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,159 @@
+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
\ No newline at end of file