diff -r 0fb910f62bf9 -r 141751cab5b2 ProgTutorial/First_Steps.thy --- a/ProgTutorial/First_Steps.thy Wed Oct 26 13:18:51 2011 +0100 +++ b/ProgTutorial/First_Steps.thy Wed Oct 26 13:19:09 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 "\ \ \"} 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 \ ?Q) \ ?R) = (?P \ ?Q \ ?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 \ 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