# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1233851645 0
# Node ID 018bfa71898209d70789ad3c217605b2f65eac0f
# Parent  7235374f34c85b66073b5bac0663fab74ace7c67
(re)defined the document antiquotation @subgoal in order to be closer to what is actually printed

diff -r 7235374f34c8 -r 018bfa718982 CookBook/antiquote_setup.ML
--- 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;
diff -r 7235374f34c8 -r 018bfa718982 CookBook/chunks.ML
--- a/CookBook/chunks.ML	Wed Feb 04 20:26:38 2009 +0000
+++ b/CookBook/chunks.ML	Thu Feb 05 16:34:05 2009 +0000
@@ -26,9 +26,14 @@
     #> space_implode "\\isasep\\isanewline%\n"
     #> enclose "\\isa{" "}");
 
+fun output pretty src ctxt = output_list pretty src ctxt o single
+
 val _ = ThyOutput.add_options
  [("gray", Library.setmp gray o boolean)]
 
+
+
+
 (** theory data **)
 
 structure ChunkData = TheoryDataFun