--- a/src/Tools/jEdit/src/document_model.scala Thu Mar 01 14:48:32 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Thu Mar 01 15:16:20 2012 +0100
@@ -63,9 +63,12 @@
def node_header(): Document.Node_Header =
{
Swing_Thread.require()
- if (Isabelle.jedit_buffer(name.node) == Some(buffer))
- Exn.capture { Isabelle.thy_load.check_thy(name) }
- else Exn.Exn(ERROR("Bad theory header")) // FIXME odd race condition!?
+ Isabelle.buffer_lock(buffer) {
+ Exn.capture {
+ Isabelle.thy_load.check_header(name,
+ Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
+ }
+ }
}