src/Pure/Isar/outer_syntax.ML

 signature BASIC_OUTER_SYNTAX =
 sig
   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
       val sync_main: unit -> unit
       val sync_loop: unit -> unit

   gen_loop term no_pos);
 
 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;
   fun sync_main () = gen_main true true;
   fun sync_loop () = gen_loop true true;