diff -r d3fcc1a0272c -r 90bee31628dc CookBook/antiquote_setup.ML
--- a/CookBook/antiquote_setup.ML	Thu Feb 26 13:46:05 2009 +0100
+++ b/CookBook/antiquote_setup.ML	Thu Mar 12 08:11:02 2009 +0100
@@ -48,9 +48,9 @@
 val output_fn = Chunks.output_list (fn _ => fn s => Pretty.str s)
 
 (* checks and prints open expressions *)
-fun output_ml src node =
+fun output_ml () =
 let
-  fun output src ctxt ((txt,ovars),pos) =
+  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))
 
@@ -58,62 +58,63 @@
       (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
        Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) []))) 
 in
-  ThyOutput.args parser output src node
+  ThyOutput.antiquotation "ML" parser output
 end
 
 (* checks and prints types and structures *)
-fun output_exp ml src node =
+fun output_exp ml =
 let 
-  fun output src ctxt (txt,pos) = 
+  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.args single_arg output src node
+  ThyOutput.antiquotation "ML_type" single_arg output
 end
 
 (* checks and expression agains a result pattern *)
-fun output_ml_response src node =
+fun output_ml_response () =
 let
-  fun output src ctxt ((lhs,pat),pos) = 
+  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.args two_args output src node
+  ThyOutput.antiquotation "ML_response" two_args output
 end
 
 (* checks the expressions, but does not check it against a result pattern *)
-fun output_ml_response_fake src node =
+fun output_ml_response_fake () =
 let
-  fun output src ctxt ((lhs,pat),pos) = 
+  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.args two_args output src node
+  ThyOutput.antiquotation "ML_response_fake" two_args output
 end
 
 (* just prints an expression and a result pattern *)
-fun output_ml_response_fake_both src node =
+fun output_ml_response_fake_both () =
 let 
-  fun ouput src ctxt ((lhs,pat), _) = 
+  fun ouput {state: Toplevel.state, source = src, context = ctxt}   ((lhs,pat), _) = 
     output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))
 in
-  ThyOutput.args two_args ouput src node
+  ThyOutput.antiquotation "ML_response_fake_both" two_args ouput
 end
 
 (* checks whether a file exists in the Isabelle distribution *)
-fun check_file_exists src node =
+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.args (Scan.lift Args.name)
-      (ThyOutput.output (fn _ => fn s => (check s; Pretty.str s))) src node
+  ThyOutput.antiquotation "ML_file" (Scan.lift Args.name)
+      (fn _ => fn s => (check s; ThyOutput.output [Pretty.str s]))
 end
 
 (* replaces the official subgoal antiquotation with one *)
 (* that is closer to the actual output                  *)
-fun output_goals src node = 
+(*
+fun output_goals  {state = node, source: Args.src, context: Proof.context}  _ = 
 let 
   fun subgoals 0 = ""
     | subgoals 1 = "goal (1 subgoal):"
@@ -129,22 +130,22 @@
 
   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 
-  ThyOutput.args (Scan.succeed ()) 
-   (Chunks.output (fn _ => fn _ => Pretty.chunks output)) src node
+  output 
 end
+*)
+
 
-val _ = ThyOutput.add_commands
-  [("ML", output_ml),
-   ("ML_file", check_file_exists),
-   ("ML_response", output_ml_response),
-   ("ML_response_fake", output_ml_response_fake),
-   ("ML_response_fake_both", output_ml_response_fake_both),
-   ("ML_struct", output_exp ml_struct),
-   ("ML_type", output_exp ml_type),
-   ("subgoals", output_goals)];
+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*)
    
 end;