# HG changeset patch
# User nipkow
# Date 972891277 -3600
# Node ID 813a4e8f12769bc87c68fca3ed34a6cd144390e7
# Parent  78434c9a54fde9ca461049e367ceecc858c4db1f
Added antiquotation "subgoals".

diff -r 78434c9a54fd -r 813a4e8f1276 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Mon Oct 30 08:34:12 2000 +0100
+++ b/src/Pure/Isar/isar_output.ML	Mon Oct 30 08:34:37 2000 +0100
@@ -292,10 +292,11 @@
 fun pretty_thm ctxt thms =
   Pretty.chunks (map (pretty_term ctxt o #prop o Thm.rep_thm) thms);
 
-fun pretty_goals state _ _ =
-  Pretty.chunks (Proof.pretty_goals (Toplevel.proof_of state handle Toplevel.UNDEF =>
-    error "No proof state"));
-
+fun pretty_goals state print_goal _ _ =
+  Pretty.chunks (Proof.pretty_goals (Toplevel.proof_of state
+                                     handle Toplevel.UNDEF
+                                        => error "No proof state")
+                                    print_goal);
 
 fun output_with pretty src ctxt x =
   let
@@ -312,7 +313,9 @@
   ("term", args Args.local_term (output_with pretty_term)),
   ("typ", args Args.local_typ_no_norm (output_with pretty_typ)),
   ("goals", fn src => fn state =>
-      args (Scan.succeed ()) (output_with (pretty_goals state)) src state)];
+      args (Scan.succeed ()) (output_with (pretty_goals state true)) src state),
+  ("subgoals", fn src => fn state =>
+      args (Scan.succeed ()) (output_with (pretty_goals state false)) src state)];
 
 end;
 
diff -r 78434c9a54fd -r 813a4e8f1276 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Oct 30 08:34:12 2000 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Oct 30 08:34:37 2000 +0100
@@ -43,7 +43,7 @@
   val pretty_thms: thm list -> Pretty.T
   val verbose: bool ref
   val print_state: int -> state -> unit
-  val pretty_goals: state -> Pretty.T list
+  val pretty_goals: state -> bool -> Pretty.T list
   val level: state -> int
   type method
   val method: (thm list -> tactic) -> method
@@ -352,9 +352,9 @@
       else pretty_goal (find_goal 0 state))
   in Pretty.writeln (Pretty.chunks prts) end;
 
-fun pretty_goals state =
+fun pretty_goals state print_goal =
   let val (_, (_, ((_, (_, thm)), _))) = find_goal 0 state
-  in Locale.pretty_goals (! goals_limit) thm end;
+  in Locale.pretty_sub_goals print_goal (!goals_limit) thm end;