--- a/ProgTutorial/First_Steps.thy Mon Oct 17 13:30:49 2011 +0100
+++ b/ProgTutorial/First_Steps.thy Wed Oct 19 21:57:22 2011 +0100
@@ -57,21 +57,13 @@
\end{graybox}
\end{isabelle}
- If you work with ProofGeneral then like normal Isabelle scripts
- \isacommand{ML}-commands can be evaluated by
- using the advance and undo buttons of your Isabelle environment. The code
- inside the \isacommand{ML}-command can also contain value and function
- bindings, for example
-*}
+ If you work with ProofGeneral then like normal Isabelle scripts
+ \isacommand{ML}-commands can be evaluated by using the advance and
+ undo buttons of your Isabelle environment. If you work with the
+ Jedit GUI, then you just have to hover the cursor over the code
+ and you see the evaluated result in the ``Output'' window.
-ML %gray {*
- val r = Unsynchronized.ref 0
- fun f n = n + 1
-*}
-
-text {*
- and even those can be undone when the proof script is retracted. As
- mentioned in the Introduction, we will drop the \isacommand{ML}~@{text
+ As mentioned in the Introduction, we will drop the \isacommand{ML}~@{text
"\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we show code. The lines
prefixed with @{text [quotes] ">"} are not part of the code, rather they
indicate what the response is when the code is evaluated. There are also
@@ -140,8 +132,8 @@
@{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
- will print out @{text [quotes] "any string"} inside the response buffer of
- Isabelle. This function expects a string as argument. If you develop under
+ will print out @{text [quotes] "any string"} inside the response buffer.
+ This function expects a string as argument. If you develop under
PolyML, then there is a convenient, though again ``quick-and-dirty'', method
for converting values into strings, namely the antiquotation
@{text "@{make_string}"}:
@@ -162,11 +154,8 @@
This function raises the exception @{text ERROR}, which will then
be displayed by the infrastructure. Note that this exception is meant
for ``user-level'' error messages seen by the ``end-user''.
-
For messages where you want to indicate a genuine program error, then
- use the exception @{text Fail}. Here the infrastructure indicates that this
- is a low-level exception, and also prints the source position of the ML
- raise statement.
+ use the exception @{text Fail}.
Most often you want to inspect data of Isabelle's basic data structures,
namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
@@ -324,15 +313,15 @@
\emph{not} print out information as
@{ML_response_fake [display,gray]
-"writeln \"First half,\";
-writeln \"and second half.\""
+"pwriteln (Pretty.str \"First half,\");
+pwriteln (Pretty.str \"and second half.\")"
"First half,
and second half."}
but as a single string with appropriate formatting. For example
@{ML_response_fake [display,gray]
-"writeln (\"First half,\" ^ \"\\n\" ^ \"and second half.\")"
+"pwriteln (Pretty.str (\"First half,\" ^ \"\\n\" ^ \"and second half.\"))"
"First half,
and second half."}
@@ -342,7 +331,7 @@
and inserts newlines in between each element.
@{ML_response_fake [display, gray]
- "writeln (cat_lines [\"foo\", \"bar\"])"
+ "pwriteln (Pretty.str (cat_lines [\"foo\", \"bar\"]))"
"foo
bar"}
@@ -502,7 +491,7 @@
is often used for setup functions inside the
\isacommand{setup}-command. These functions have to be of type @{ML_type
"theory -> theory"}. More than one such setup function can be composed with
- @{ML "#>"}.\footnote{give example}
+ @{ML "#>"}.\footnote{TBD: give example}
The remaining combinators we describe in this section add convenience for the
``waterfall method'' of writing functions. The combinator @{ML_ind tap in
@@ -512,7 +501,7 @@
ML %linenosgray{*fun inc_by_three x =
x |> (fn x => x + 1)
- |> tap (fn x => writeln (@{make_string} x))
+ |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
|> (fn x => x + 2)*}
text {*
@@ -788,7 +777,7 @@
((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}
The thm-antiquotations can also be used for manipulating theorems. For
- example, if you need the version of te theorem @{thm [source] refl} that
+ example, if you need the version of the theorem @{thm [source] refl} that
has a meta-equality instead of an equality, you can write
@{ML_response_fake [display,gray]
@@ -864,6 +853,10 @@
ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat)
end*}
+text {*
+ To use it you also have to install it using \isacommand{setup} like so
+*}
+
setup{* term_pat_setup *}
text {*
@@ -878,7 +871,7 @@
"Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
which shows the internal representation of the term @{text "Suc ?x"}. Similarly
- we can write an antiquotation for type patterns.
+ we can write an antiquotation for type patterns. Its code is
*}
ML{*val type_pat_setup =
@@ -893,9 +886,17 @@
ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat)
end*}
+text {*
+ which can be installed with
+*}
+
setup{* type_pat_setup *}
text {*
+ However, a word of warning is in order: Introducing new antiquotations
+ should be done only after careful deliberations. They can make your
+ code harder to read, than making it easier.
+
\begin{readmore}
The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
for most antiquotations. Most of the basic operations on ML-syntax are implemented
@@ -919,7 +920,7 @@
some \emph{fixed} collection of types. In light of the conventional wisdom cited
above it is important to keep in mind that the universal type does not
destroy type-safety of ML: storing and accessing the data can only be done
- in a type-safe manner.
+ in a type-safe manner...though run-time checks are needed for that.
\begin{readmore}
In Isabelle the universal type is implemented as the type @{ML_type
@@ -950,7 +951,7 @@
ML{*val foo_list =
let
- val thirteen = inject_int 13
+ val thirteen = inject_int 13
val truth_val = inject_bool true
in
[thirteen, truth_val]
@@ -1115,7 +1116,9 @@
"WrongRefData.get @{theory}"
"ref [1, 1]"}
- Now imagine how often you go backwards and forwards in your proof scripts.
+ Now imagine how often you go backwards and forwards in your proof
+ scripts.\footnote{The same problem can be triggered in the Jedit GUI by
+ making the parser to go over and over again over the \isacommand{setup} command.}
By using references in Isabelle code, you are bound to cause all
hell to break loose. Therefore observe the coding convention:
Do not use references for storing data!
@@ -1149,7 +1152,7 @@
fun print ctxt =
case (Data.get ctxt) of
- [] => writeln "Empty!"
+ [] => pwriteln (Pretty.str "Empty!")
| trms => pwriteln (pretty_terms ctxt trms)*}
text {*
@@ -1312,7 +1315,7 @@
A concrete example for a configuration value is
@{ML_ind simp_trace in Raw_Simplifier}, which switches on trace information
- in the simplifier. This can be used as in the following proof
+ in the simplifier. This can be used for example in the following proof
*}
lemma