1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Nov 17 02:19:51 2006 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Nov 17 02:19:52 2006 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4        val state: unit -> Toplevel.state
     1.5        val exn: unit -> (exn * string) option
     1.6        val context: unit -> Proof.context
     1.7 +      val goal: unit -> thm list * thm
     1.8        val main: unit -> unit
     1.9        val loop: unit -> unit
    1.10        val sync_main: unit -> unit
    1.11 @@ -325,9 +326,15 @@
    1.12  struct
    1.13    val state = Toplevel.get_state;
    1.14    val exn = Toplevel.exn;
    1.15 +
    1.16    fun context () =
    1.17      Context.proof_of (Toplevel.context_of (state ()))
    1.18        handle Toplevel.UNDEF => error "Unknown context";
    1.19 +
    1.20 +  fun goal () =
    1.21 +    #2 (Proof.get_goal (Toplevel.proof_of (state ())))
    1.22 +      handle Toplevel.UNDEF => error "No goal present";
    1.23 +
    1.24    fun main () = gen_main false false;
    1.25    fun loop () = gen_loop false false;
    1.26    fun sync_main () = gen_main true true;