--- a/CookBook/antiquote_setup.ML	Wed Feb 04 20:26:38 2009 +0000
+++ b/CookBook/antiquote_setup.ML	Thu Feb 05 16:34:05 2009 +0000
@@ -57,6 +57,27 @@
   if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then ()
   else error ("Source file " ^ quote txt ^ " does not exist.")
 
+(* to be closer to the actual output *)
+fun output_goals main_goal src node = 
+let 
+  fun subgoals 0 = "No subgoals!"
+    | 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");
+
+  val state = proof_state node
+  val goals = Proof.pretty_goals main_goal state;
+  val msg  = Pretty.str (subgoals (length goals))  
+in 
+  ThyOutput.args (Scan.succeed ()) 
+   (Chunks.output (fn _ => fn _ => Pretty.chunks (msg::goals))) src node
+end
+
+
 val _ = ThyOutput.add_commands
   [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name --
       (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
@@ -73,6 +94,7 @@
    ("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
       (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))];
+   ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type)),
+   ("subgoals", output_goals false)];
    
 end;