
diff -r e21b2f888fa2 -r 631d12c25bde CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Tue Oct 14 01:33:55 2008 -0400
+++ b/CookBook/FirstSteps.thy	Fri Oct 17 05:02:04 2008 -0400
@@ -14,7 +14,7 @@
 
   \begin{center}
   \begin{tabular}{@ {}l}
-  \isacommand{theory} CookBook\\
+  \isacommand{theory} FirstSteps\\
   \isacommand{imports} Main\\
   \isacommand{begin}\\
   \ldots
@@ -26,29 +26,31 @@
 
 text {*
   The easiest and quickest way to include code in a theory is
-  by using the \isacommand{ML} command. For example
-*}
+  by using the \isacommand{ML} command. For example\smallskip
 
-ML {*
-  3 + 4
-*}
+\isacommand{ML}
+@{ML_text "{"}@{ML_text "*"}\isanewline
+\hspace{5mm}@{ML "3 + 4"}\isanewline
+@{ML_text "*"}@{ML_text "}"}\isanewline
+@{ML_text "> 7"}\smallskip
 
-text {*
   Expressions inside \isacommand{ML} commands are immediately evaluated,
   like ``normal'' Isabelle proof scripts, 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. However on such \isacommand{ML}
   commands the undo operation behaves slightly counter-intuitive, because 
-  if you define
-*}
+  if you define\smallskip
+ 
+\isacommand{ML}
+@{ML_text "{"}@{ML_text "*"}\isanewline
+@{ML_text "val foo = true"}\isanewline
+@{ML_text "*"}@{ML_text "}"}\isanewline
+@{ML_text "> true"}\smallskip
 
-ML {*
-  val foo = true
-*}
-
-text {*
   then Isabelle's undo operation has no effect on the definition of 
-  @{ML "foo"}. 
+  @{ML_text "foo"}. Note that from now on we will drop the 
+  \isacommand{ML} @{ML_text "{"}@{ML_text "* \<dots> *"}@{ML_text "}"} whenever
+  we show code.
 
   Once a portion of code is relatively stable, one usually wants to 
   export it to a separate ML-file. Such files can then be included in a 
@@ -63,6 +65,9 @@
   \ldots
   \end{tabular}
   \end{center}
+
+  Note that from now on we are going to drop the the  
+  
 *}
 
 section {* Debugging and Printing *}
@@ -72,40 +77,30 @@
   During developments you might find it necessary to quickly inspect some data
   in your code. This can be done in a ``quick-and-dirty'' fashion using 
   the function @{ML "warning"}. For example 
-*}
 
-ML {* warning "any string" *}
+  @{ML [display] "warning \"any string\""}
 
-text {*
-  will print out @{ML "\"any string\""} inside the response buffer of Isabelle.
+  will print out @{ML_text "\"any string\""} inside the response buffer of Isabelle.
   If you develop under PolyML, then there is a convenient, though again 
   ``quick-and-dirty'', method for converting values into strings, 
   for example: 
-*}
 
-ML {* warning (makestring 1) *}
+  @{ML [display] "warning (makestring 1)"} 
 
-text {*
   However this only works if the type of what is converted is monomorphic and not 
   a function.
-*}
 
-text {* 
-  The funtion warning should only be used for testing purposes, because
-  any output this funtion generates will be overwritten, as soon as an error 
-  is raised. 
-  Therefore for printing anything more serious and elaborate, the function @{ML tracing}
-  should be used. This function writes all output into a separate buffer.
-*}
+  The funtion warning should only be used for testing purposes, because any
+  output this funtion generates will be overwritten, as soon as an error is
+  raised. Therefore for printing anything more serious and elaborate, the
+  function @{ML tracing} should be used. This function writes all output into
+  a separate buffer.
 
-ML {* tracing "foo" *}
-
-text {* 
+  @{ML [display] "tracing \"foo\""}
 
   It is also possible to redirect the channel where the @{ML_text "foo"} is 
   printed to a separate file, e.g. to prevent Proof General from choking on massive 
   amounts of trace output. This rediretion can be achieved using the code
-
 *}
 
 ML {*
@@ -124,7 +119,7 @@
 *}
 
 text {* 
-  Calling @{ML_text "redirect_tracing"} with @{ML_text "(TextIO.openOut \"foo.bar\")"} 
+  Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 
   will cause that all tracing information is printed into the file @{ML_text "foo.bar"}.
 
 *}
@@ -138,15 +133,13 @@
   on the logical level of Isabelle. This is done using antiquotations.
   For example, one can print out the name of 
   the current theory by typing
-*}
-
-ML {* Context.theory_name @{theory} *}
-
-text {* 
+  
+  @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps : string"}
+ 
   where @{text "@{theory}"} is an antiquotation that is substituted with the
   current theory (remember that we assumed we are inside the theory CookBook). 
-  The name of this theory can be extracted using the function @{ML "Context.theory_name"}. 
-  So the code above returns the string @{ML "\"CookBook\""}.
+  The name of this theory can be extracted using the function 
+  @{ML "Context.theory_name"}. 
 
   Note, however, that antiquotations are statically scoped, that is the value is
   determined at ``compile-time'', not ``run-time''. For example the function
@@ -160,19 +153,18 @@
 text {*
   does \emph{not} return the name of the current theory, if it is run in a 
   different theory. Instead, the code above defines the constant function 
-  that always returns the string @{ML "\"CookBook\""}, no matter where the
+  that always returns the string @{ML_text "FirstSteps"}, no matter where the
   function is called. Operationally speaking,  @{text "@{theory}"} is 
   \emph{not} replaced with code that will look up the current theory in 
   some data structure and return it. Instead, it is literally
   replaced with the value representing the theory name.
 
   In a similar way you can use antiquotations to refer to theorems or simpsets:
-*}
+
 
-ML {* @{thm allI} *}
-ML {* @{simpset} *}
+  @{ML [display] "@{thm allI}"}
+  @{ML [display] "@{simpset}"}
 
-text {*
   In the course of this introduction, we will learn more about 
   these antiquotations: they greatly simplify Isabelle programming since one
   can directly access all kinds of logical elements from ML.
@@ -184,14 +176,13 @@
 text {*
   One way to construct terms of Isabelle on the ML level is by using the antiquotation 
   \mbox{@{text "@{term \<dots>}"}}:
-*}
 
-ML {* @{term "(a::nat) + b = c"} *}
+  @{ML_response [display] "@{term \"(a::nat) + b = c\"}" 
+                          "Const (\"op =\", \<dots>)  $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
-text {*
   This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal
   representation of this term. This internal representation corresponds to the 
-  datatype @{ML_text "term"}.
+  datatype @{ML_type "term"}.
   
   The internal representation of terms uses the usual de Bruijn index mechanism where bound 
   variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
@@ -225,34 +216,33 @@
   can use the following ML funtion to set the limit to a value high 
   enough:
   \end{exercise}
-*}
-ML {* print_depth 50 *}
 
-text {*
-  
+  @{ML [display] "print_depth 50"}
+
   The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 
   inserting the invisible @{text "Trueprop"} coercions whenever necessary. 
   Consider for example
 
-*}
-
-ML {* @{term "P x"} ; @{prop "P x"} *}
+  @{ML_response [display] "@{term \"P x\"}" "Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)"}
+  @{ML_response [display] "@{prop \"P x\"}" 
+                          "Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>))"}
 
-text {* which inserts the coercion in the latter case and *}
-
+  which inserts the coercion in the latter case and 
 
-ML {* @{term "P x \<Longrightarrow> Q x"} ; @{prop "P x \<Longrightarrow> Q x"} *}
+  @{ML_response [display] "@{term \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"}
+  @{ML_response [display] "@{prop \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"}
 
-text {* 
   which does not. 
 
   Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example
   
   *}
 
-ML {* @{typ "bool \<Rightarrow> nat"} *}
 
 text {*
+
+  @{ML_response [display] "@{typ \"bool \<Rightarrow> nat\"}" "Type \<dots>"}
+
   (FIXME: Unlike the term antiquotation, @{text "@{typ \<dots>}"} does not print the
   internal representation. Is there a reason for this, that needs to be explained 
   here?)
@@ -265,8 +255,6 @@
   *}
 
 
-
-
 section {* Constructing Terms and Types Manually *} 
 
 text {*
@@ -369,25 +357,23 @@
   Type checking is always relative to a theory context. For now we can use
   the @{ML "@{theory}"} antiquotation to get hold of the current theory.
   For example we can write:
-*}
+
+  (FIXME ML-response-unchecked needed)
 
-ML {* cterm_of @{theory} @{term "(a::nat) + b = c"} *}
+  @{ML [display] "@{term \"(a::nat) + b = c\"}"}
 
-text {* and *}
+  and 
 
-ML {*
-  let
-    val natT = @{typ "nat"}
-    val zero = @{term "0::nat"}
-  in
-    cterm_of @{theory} 
-        (Const (@{const_name plus}, natT --> natT --> natT) 
-         $ zero $ zero)
-  end
-*}
+@{ML [display] 
+"let
+  val natT = @{typ \"nat\"}
+  val zero = @{term \"0::nat\"}
+in
+  cterm_of @{theory} 
+  (Const (@{const_name plus}, natT --> natT --> natT) 
+  $ zero $ zero)
+end"}
 
-text {*
-  
   \begin{exercise}
   Check that the function defined in Exercise~\ref{fun:revsum} returns a
   result that type checks.
@@ -574,5 +560,61 @@
 
 section {* Theorem Attributes *}
 
+ML {* 
+  val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;
+
+fun ml_val ys txt = "fn " ^
+  (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^
+  " => (" ^ txt ^ ");";
+
+fun ml_val_open (ys, []) txt = ml_val ys txt
+  | ml_val_open (ys, xs) txt =
+      ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end");
+
+fun ml_pat (rhs, pat) =
+  let val pat' = implode (map (fn "\\<dots>" => "_" | s => s)
+    (Symbol.explode pat))
+  in
+    "val " ^ pat' ^ " = " ^ rhs
+  end;
+
+(* modified from original *)
+fun ml_val txt = "fn _ => (" ^ txt ^ ");";
+fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;";
+fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
+
+*}
+
+ML {* ml_pat *}
+ML {* K ml_pat *}
+
+ML {*
+fun output_verbatim ml src ctxt (txt, pos) =
+  let val txt = ml ctxt (txt, pos)
+  in
+    (if ! ThyOutput.source then str_of_source src else txt)
+    |> (if ! ThyOutput.quotes then quote else I)
+    |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt
+  end;
+*}
+
+ML {*
+fun output_ml ml = output_verbatim
+  (fn ctxt => fn ((txt, p), pos) =>
+     (ML_Context.eval_in (SOME ctxt) false pos (ml p txt);
+      txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |>
+      Chunks.transform_cmts |> implode));
+*}
+
+ML {* 
+fun output_ml_checked ml src ctxt (txt, pos) =
+ (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
+ (if ! ThyOutput.source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
+  |> (if ! ThyOutput.quotes then quote else I)
+  |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt)
+
+*}
+
+
 
 end
\ No newline at end of file




