# HG changeset patch
# User wenzelm
# Date 1330554695 -3600
# Node ID 1d2cbcc50fb2844f321757d6181cf7ac353e0b06
# Parent  09ab89658a5d783f7f662da88ef02e0e9eed31b4
more defensive node_header;

diff -r 09ab89658a5d -r 1d2cbcc50fb2 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Feb 29 23:09:06 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Feb 29 23:31:35 2012 +0100
@@ -63,8 +63,9 @@
   def node_header(): Document.Node_Header =
   {
     Swing_Thread.require()
-    // FIXME assert(Isabelle.jedit_buffer(name.node) == Some(buffer))
-    Exn.capture { session.thy_load.check_thy(name) }
+    if (Isabelle.jedit_buffer(name.node) == Some(buffer))
+      Exn.capture { session.thy_load.check_thy(name) }
+    else Exn.Exn(ERROR("Bad theory header"))  // FIXME odd race condition!?
   }