--- a/CookBook/FirstSteps.thy	Thu Mar 12 08:11:02 2009 +0100
+++ b/CookBook/FirstSteps.thy	Thu Mar 12 14:25:35 2009 +0000
@@ -169,11 +169,7 @@
 end
 
 fun str_of_thm ctxt thm =
-let
-  val {prop, ...} = crep_thm (no_vars ctxt thm)
-in 
-  str_of_cterm ctxt prop
-end*}
+  str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}
 
 text {* 
   Again the function @{ML commas} helps with printing more than one theorem. 
@@ -533,7 +529,7 @@
 
 ML{*fun make_imp P Q tau =
 let
-  val x = Free ("x",tau)
+  val x = Free ("x", tau)
 in 
   Logic.all x (Logic.mk_implies (P $ x, Q $ x))
 end *}

--- a/CookBook/Recipes/Antiquotes.thy	Thu Mar 12 08:11:02 2009 +0100
+++ b/CookBook/Recipes/Antiquotes.thy	Thu Mar 12 14:25:35 2009 +0000
@@ -46,13 +46,13 @@
 
 text {*
 
-  Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, 
+  The parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, 
   in this case the code. As mentioned before, the code
   is sent to the ML-compiler in the line 4 using the function @{ML ml_val},
   which constructs the appropriate ML-expression.
   If the code is ``approved'' by the compiler, then the output function @{ML
   "ThyOutput.output"} in the next line pretty prints the
-  code. This function expects that the code is a list of strings where each
+  code. This function expects that the code is a list of (pretty)strings where each
   string correspond to a line in the output. Therefore the use of 
   @{ML "(space_explode \"\\n\" txt)" for txt} 
   which produces this list according to linebreaks.  There are a number of options 
@@ -69,7 +69,7 @@
   can improve the code above slightly by writing 
 *}
 
-ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt,pos) =
+ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) =
   (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt);
    ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
 
@@ -77,7 +77,9 @@
          (Scan.lift (OuterParse.position Args.name)) output_ml *}
 
 text {*
-  where in Lines 1 and 2 the positional information is properly treated.
+  where in Lines 1 and 2 the positional information is properly treated. The
+  parser @{ML OuterParse.position} encodes the positional information in the 
+  result.
 
   We can now write in a document @{text "@{ML_checked \"2 + 3\"}"} in order to
   obtain @{ML_checked "2 + 3"} and be sure that this code compiles until

--- a/CookBook/antiquote_setup.ML	Thu Mar 12 08:11:02 2009 +0100
+++ b/CookBook/antiquote_setup.ML	Thu Mar 12 14:25:35 2009 +0000
@@ -4,7 +4,6 @@
 struct
 
 (* functions for generating appropriate expressions *)
-
 fun ml_val_open (ys, xs) txt = 
   let fun ml_val_open_aux ys txt = 
           "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
@@ -25,8 +24,8 @@
 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";
 
 (* eval function *)
-fun eval_fn ctxt pos exp =
-  ML_Context.eval_in (SOME ctxt) false pos exp
+fun eval_fn ctxt exp =
+  ML_Context.eval_in (SOME ctxt) false Position.none exp
 
 (* string functions *)
 fun string_explode str txt =
@@ -40,112 +39,82 @@
   #> implode 
   #> string_explode "";
 
-(* parser for single and two arguments *)
-val single_arg = Scan.lift (OuterParse.position Args.name)
-val two_args = Scan.lift (OuterParse.position (Args.name -- Args.name))
-
 (* output function *)
-val output_fn = Chunks.output_list (fn _ => fn s => Pretty.str s)
+fun output_fn txt =  Chunks.output (map Pretty.str txt)
 
 (* checks and prints open expressions *)
-fun output_ml () =
-let
-  fun output {state: Toplevel.state, source = src, context = ctxt} ((txt,ovars),pos) =
-    (eval_fn ctxt pos (ml_val_open ovars txt);
-     output_fn src ctxt (transform_cmts_str txt))
+fun output_ml {context = ctxt, ...} (txt, ovars) =
+  (eval_fn ctxt (ml_val_open ovars txt);
+   output_fn (transform_cmts_str txt))
 
-  val parser = Scan.lift (OuterParse.position (Args.name --
-      (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
-       Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) []))) 
-in
-  ThyOutput.antiquotation "ML" parser output
-end
+val parser_ml = Scan.lift (Args.name --
+  (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
+   Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])) 
 
 (* checks and prints types and structures *)
-fun output_exp ml =
-let 
-  fun output {state: Toplevel.state, source = src, context = ctxt} (txt,pos) = 
-    (eval_fn ctxt pos (ml txt);
-     output_fn src ctxt (string_explode "" txt))
-in
-  ThyOutput.antiquotation "ML_type" single_arg output
-end
+fun output_exp ml {context = ctxt, ...} txt = 
+  (eval_fn ctxt (ml txt);
+   output_fn (string_explode "" txt))
 
 (* checks and expression agains a result pattern *)
-fun output_ml_response () =
-let
-  fun output {state: Toplevel.state, source = src, context = ctxt} ((lhs,pat),pos) = 
-    (eval_fn ctxt pos (ml_pat (lhs,pat));
-     output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)))
-in
-  ThyOutput.antiquotation "ML_response" two_args output
-end
+fun output_response {context = ctxt, ...} (lhs, pat) = 
+    (eval_fn ctxt (ml_pat (lhs, pat));
+     output_fn ((string_explode "" lhs) @ (string_explode "> " pat)))
+
+(* checks the expressions, but does not check it against a result pattern *)
+fun output_response_fake {context = ctxt, ...} (lhs, pat) = 
+    (eval_fn ctxt (ml_val lhs);
+     output_fn ((string_explode "" lhs) @ (string_explode "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)
-fun output_ml_response_fake () =
-let
-  fun output {state: Toplevel.state, source = src, context = ctxt} ((lhs, pat), pos) = 
-    (eval_fn ctxt pos (ml_val lhs);
-     output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)))
-in
-  ThyOutput.antiquotation "ML_response_fake" two_args output
-end
+fun ouput_response_fake_both _ (lhs, pat) = 
+    output_fn ((string_explode "" lhs) @ (string_explode "> " pat))
+
+val single_arg = Scan.lift (Args.name)
+val two_args   = Scan.lift (Args.name -- Args.name)
 
-(* just prints an expression and a result pattern *)
-fun output_ml_response_fake_both () =
-let 
-  fun ouput {state: Toplevel.state, source = src, context = ctxt}   ((lhs,pat), _) = 
-    output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))
-in
-  ThyOutput.antiquotation "ML_response_fake_both" two_args ouput
-end
+val _ = ThyOutput.antiquotation "ML" parser_ml output_ml
+val _ = ThyOutput.antiquotation "ML_type" single_arg (output_exp ml_type)
+val _ = ThyOutput.antiquotation "ML_struct" single_arg (output_exp ml_struct)
+val _ = ThyOutput.antiquotation "ML_response" two_args output_response
+val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake
+val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both
 
 (* checks whether a file exists in the Isabelle distribution *)
-fun check_file_exists () =
-let 
-  fun check txt =
-   if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then ()
-   else error ("Source file " ^ (quote txt) ^ " does not exist.")
-in
-  ThyOutput.antiquotation "ML_file" (Scan.lift Args.name)
-      (fn _ => fn s => (check s; ThyOutput.output [Pretty.str s]))
-end
+fun check_file_exists _ txt =
+  (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
+   then output_fn (string_explode "" txt)
+   else error ("Source file " ^ (quote txt) ^ " does not exist."))
+
+val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists
+
 
 (* replaces the official subgoal antiquotation with one *)
 (* that is closer to the actual output                  *)
-(*
-fun output_goals  {state = node, source: Args.src, context: Proof.context}  _ = 
-let 
+fun output_goals  {state = node, ...}  _ = 
+let
   fun subgoals 0 = ""
     | subgoals 1 = "goal (1 subgoal):"
-    | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):";
- 
-  fun proof_state node =
-     (case Option.map Toplevel.proof_node node of
-          SOME (SOME prf) => ProofNode.current prf
-        | _ => error "No proof state");
+    | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"
+
+  fun proof_state state =
+    (case try Toplevel.proof_of state of
+      SOME prf => prf
+    | _ => error "No proof state")
 
   val state = proof_state node;
   val goals = Proof.pretty_goals false state;
 
   val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);
   val (As, B) = Logic.strip_horn prop;
-  val output'  = (case (length As) of
+  val output  = (case (length As) of
                       0 => goals 
                     | n => (Pretty.str (subgoals n))::goals)  
 in 
-  output 
+  ThyOutput.output output
 end
-*)
 
 
-val _ = output_ml ();
-val _ = check_file_exists ();
-val _ = output_ml_response ();
-val _ = output_ml_response_fake ();
-val _ = output_ml_response_fake_both ();
-val _ = output_exp ml_struct;
-val _ = output_exp ml_type;
-(*val _ = output_goals*)
+val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals
    
 end;

--- a/CookBook/chunks.ML	Thu Mar 12 08:11:02 2009 +0100
+++ b/CookBook/chunks.ML	Thu Mar 12 14:25:35 2009 +0000
@@ -2,20 +2,14 @@
 structure Chunks =
 struct
 
-(* rebuilding the output_list function from ThyOutput in order to *)
-(* enable the options [gray, linenos] *)
+(* rebuilding the output function from ThyOutput in order to *)
+(* enable the options [gray, linenos]                        *)
 
 val gray = ref false;
 val linenos = ref false
 
-fun boolean "" = true
-  | boolean "true" = true
-  | boolean "false" = false
-  | boolean s = error ("Bad boolean value: " ^ quote s);
-
-fun output_list pretty src ctxt xs =
-  map (pretty ctxt) xs        (*always pretty in order to exhibit errors!*)
-  |> (if ! ThyOutput.source then K [ThyOutput.pretty_text (ThyOutput.str_of_source src)] else I)
+fun output prts =
+  prts
   |> (if ! ThyOutput.quotes then map Pretty.quote else I)
   |> (if ! ThyOutput.display then
     map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
@@ -23,12 +17,16 @@
     #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I) 
     #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) 
     #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
- else
+  else
     map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
     #> space_implode "\\isasep\\isanewline%\n"
     #> enclose "\\isa{" "}");
 
-fun output pretty src ctxt = output_list pretty src ctxt o single
+
+fun boolean "" = true
+  | boolean "true" = true
+  | boolean "false" = false
+  | boolean s = error ("Bad boolean value: " ^ quote s);
 
 val _ = ThyOutput.add_options
  [("gray", Library.setmp gray o boolean),
@@ -161,7 +159,7 @@
     val txt = spc ^ implode (transform_cmts toks')
   in
     txt |> split_lines |>
-    output_list (fn _ => fn s => Pretty.str s) src ctxt
+    (map Pretty.str) |> output 
   end;
 
 val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk;

Binary file cookbook.pdf has changed