src/Pure/Isar/outer_syntax.ML
changeset 21207 cef082634be9
parent 20323 ac413d7cc03d
child 21401 faddc6504177
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Nov 07 11:46:48 2006 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Nov 07 11:46:49 2006 +0100
     1.3 @@ -10,8 +10,8 @@
     1.4    structure Isar:
     1.5      sig
     1.6        val state: unit -> Toplevel.state
     1.7 +      val exn: unit -> (exn * string) option
     1.8        val context: unit -> Proof.context
     1.9 -      val exn: unit -> (exn * string) option
    1.10        val main: unit -> unit
    1.11        val loop: unit -> unit
    1.12        val sync_main: unit -> unit
    1.13 @@ -324,8 +324,10 @@
    1.14  structure Isar =
    1.15  struct
    1.16    val state = Toplevel.get_state;
    1.17 -  val context = Context.proof_of o Toplevel.context_of o state;
    1.18    val exn = Toplevel.exn;
    1.19 +  fun context () =
    1.20 +    Context.proof_of (Toplevel.context_of (state ()))
    1.21 +      handle Toplevel.UNDEF => error "Unknown context";
    1.22    fun main () = gen_main false false;
    1.23    fun loop () = gen_loop false false;
    1.24    fun sync_main () = gen_main true true;