added Isar.goal;

--- a/doc-src/IsarImplementation/Thy/integration.thy	Fri Nov 17 02:19:51 2006 +0100
+++ b/doc-src/IsarImplementation/Thy/integration.thy	Fri Nov 17 02:19:52 2006 +0100
@@ -284,8 +284,9 @@
   @{index_ML Isar.main: "unit -> unit"} \\
   @{index_ML Isar.loop: "unit -> unit"} \\
   @{index_ML Isar.state: "unit -> Toplevel.state"} \\
+  @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
   @{index_ML Isar.context: "unit -> Proof.context"} \\
-  @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
+  @{index_ML Isar.goal: "unit -> thm list * thm"} \\
   \end{mldecls}
 
   \begin{description}
@@ -304,6 +305,10 @@
   "Isar.state ()"}, analogous to @{ML Context.proof_of}
   (\secref{sec:generic-context}).
 
+  \item @{ML "Isar.goal ()"} picks the goal configuration from @{ML
+  "Isar.state ()"}, consisting on the current facts and the goal
+  represented as a theorem according to \secref{sec:tactical-goals}.
+
   \end{description}
 *}
 

--- a/src/Pure/Isar/outer_syntax.ML	Fri Nov 17 02:19:51 2006 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Nov 17 02:19:52 2006 +0100
@@ -12,6 +12,7 @@
       val state: unit -> Toplevel.state
       val exn: unit -> (exn * string) option
       val context: unit -> Proof.context
+      val goal: unit -> thm list * thm
       val main: unit -> unit
       val loop: unit -> unit
       val sync_main: unit -> unit
@@ -325,9 +326,15 @@
 struct
   val state = Toplevel.get_state;
   val exn = Toplevel.exn;
+
   fun context () =
     Context.proof_of (Toplevel.context_of (state ()))
       handle Toplevel.UNDEF => error "Unknown context";
+
+  fun goal () =
+    #2 (Proof.get_goal (Toplevel.proof_of (state ())))
+      handle Toplevel.UNDEF => error "No goal present";
+
   fun main () = gen_main false false;
   fun loop () = gen_loop false false;
   fun sync_main () = gen_main true true;