# HG changeset patch
# User wenzelm
# Date 1152192093 -7200
# Node ID 33124a9f5e31d71ec3e55184715c1a11944b9a4f
# Parent  b07a138b4e7d1355f311b5a4c911299660205924
added Isar.context;

diff -r b07a138b4e7d -r 33124a9f5e31 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Jul 06 12:18:17 2006 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Jul 06 15:21:33 2006 +0200
@@ -10,6 +10,7 @@
   structure Isar:
     sig
       val state: unit -> Toplevel.state
+      val context: unit -> Proof.context
       val exn: unit -> (exn * string) option
       val main: unit -> unit
       val loop: unit -> unit
@@ -323,6 +324,7 @@
 structure Isar =
 struct
   val state = Toplevel.get_state;
+  val context = Context.proof_of o Toplevel.context_of o state;
   val exn = Toplevel.exn;
   fun main () = gen_main false false;
   fun loop () = gen_loop false false;