src/Tools/jEdit/src/document_model.scala
changeset 46750 69efe9b2994c
parent 46748 8f3ae4d04a2d
child 46920 5f44c8bea84e
--- 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 */