more defensive node_header;
authorwenzelm
Wed, 29 Feb 2012 23:31:35 +0100
changeset 46738 1d2cbcc50fb2
parent 46737 09ab89658a5d
child 46739 6024353549ca
more defensive node_header;
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!?
   }