# HG changeset patch
# User wenzelm
# Date 1319035546 -7200
# Node ID b6c527c64789d3aac17f19818b57579aecaccf50
# Parent  78478d938cb8c269cbe5d434dc9dbdfa5f2d7de6
more robust toplevel_error reporting (NB: Context.proof_of on a stale theory crashes ungracefully);

diff -r 78478d938cb8 -r b6c527c64789 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Oct 19 15:42:43 2011 +0200
+++ b/src/Pure/Isar/runtime.ML	Wed Oct 19 16:45:46 2011 +0200
@@ -126,8 +126,11 @@
     if Exn.is_interrupt exn then reraise exn
     else
       let
-        val ctxt = Option.map Context.proof_of (Context.thread_data ());
-        val _ = output_exn (exn_context ctxt exn);
+        val opt_ctxt =
+          (case Context.thread_data () of
+            NONE => NONE
+          | SOME context => try Context.proof_of context);
+        val _ = output_exn (exn_context opt_ctxt exn);
       in raise TOPLEVEL_ERROR end;
 
 end;