changeset 43715 | 518e44a0ee15 |
parent 43697 | 77ce24aa1770 |
child 43718 | 4a4ca9e4a14b |
--- a/src/Tools/jEdit/src/document_model.scala Sat Jul 09 12:56:51 2011 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Sat Jul 09 13:29:33 2011 +0200 @@ -62,7 +62,7 @@ /* pending text edits */ private def node_header(): Document.Node.Header = - new Document.Node.Header(master_dir, + Document.Node.Header(master_dir, Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }) private object pending_edits // owned by Swing thread