
diff -r fea1b7ce5c4a -r 683fb6e468b1 ProgTutorial/First_Steps.thy
--- 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




