# HG changeset patch
# User wenzelm
# Date 1162896409 -3600
# Node ID cef082634be9d98716be71453b942f4a63dc6f38
# Parent  2af4c7b3f7ef6a20c7e703a627acd84350b1e28e
Isar.context: proper error;

diff -r 2af4c7b3f7ef -r cef082634be9 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Nov 07 11:46:48 2006 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Nov 07 11:46:49 2006 +0100
@@ -10,8 +10,8 @@
   structure Isar:
     sig
       val state: unit -> Toplevel.state
+      val exn: unit -> (exn * string) option
       val context: unit -> Proof.context
-      val exn: unit -> (exn * string) option
       val main: unit -> unit
       val loop: unit -> unit
       val sync_main: unit -> unit
@@ -324,8 +324,10 @@
 structure Isar =
 struct
   val state = Toplevel.get_state;
-  val context = Context.proof_of o Toplevel.context_of o state;
   val exn = Toplevel.exn;
+  fun context () =
+    Context.proof_of (Toplevel.context_of (state ()))
+      handle Toplevel.UNDEF => error "Unknown context";
   fun main () = gen_main false false;
   fun loop () = gen_loop false false;
   fun sync_main () = gen_main true true;