# HG changeset patch
# User wenzelm
# Date 1330613283 -3600
# Node ID 69efe9b2994ca0745cf56a07374765edb9ad0e2d
# Parent  042c546d2baca3bc3141197e46a8a76d0c2092ad
more robust locking;

diff -r 042c546d2bac -r 69efe9b2994c src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Mar 01 15:42:44 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Mar 01 15:48:03 2012 +0100
@@ -61,15 +61,12 @@
   /* header */
 
   def node_header(): Document.Node_Header =
-  {
-    Swing_Thread.require()
-    Isabelle.buffer_lock(buffer) {
+    Isabelle.swing_buffer_lock(buffer) {
       Exn.capture {
         Isabelle.thy_load.check_header(name,
           Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
       }
     }
-  }
 
 
   /* perspective */