diff -r 123401a5c8e9 -r 5e309df58557 CookBook/antiquote_setup.ML
--- a/CookBook/antiquote_setup.ML	Fri Feb 06 06:19:52 2009 +0000
+++ b/CookBook/antiquote_setup.ML	Sat Feb 07 12:05:02 2009 +0000
@@ -53,12 +53,19 @@
   let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
   in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end
 
-fun check_file_exists ctxt txt =
-  if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then ()
-  else error ("Source file " ^ quote txt ^ " does not exist.")
+fun check_file_exists src node =
+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
+end
 
-(* to be closer to the actual output *)
-fun output_goals main_goal src node = 
+(* replaces the official subgoal antiquotation with one *)
+(* that is closer to the actual output                  *)
+fun output_goals src node = 
 let 
   fun subgoals 0 = ""
     | subgoals 1 = "goal (1 subgoal):"
@@ -70,7 +77,7 @@
         | _ => error "No proof state");
 
   val state = proof_state node;
-  val goals = Proof.pretty_goals main_goal state;
+  val goals = Proof.pretty_goals false state;
 
   val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);
   val (As, B) = Logic.strip_horn prop;
@@ -88,10 +95,7 @@
       (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
        Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) 
                                                                  (output_ml ml_val_open)),
-   ("ML_file", ThyOutput.args (Scan.lift Args.name)
-      (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))),
-   ("ML_text", ThyOutput.args (Scan.lift Args.name)
-      (ThyOutput.output (fn _ => fn s => Pretty.str s))),
+   ("ML_file", check_file_exists),
    ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
       (output_ml_response ml_pat)),
    ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
@@ -100,6 +104,6 @@
       (output_ml_response_fake_both ml_val)),
    ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)),
    ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type)),
-   ("subgoals", output_goals false)];
+   ("subgoals", output_goals)];
    
 end;