author | wenzelm |
Thu, 01 Mar 2012 15:48:03 +0100 | |
changeset 46750 | 69efe9b2994c |
parent 46749 | 042c546d2bac |
child 46754 | e33519ec9e91 |
--- 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 */