src/Tools/jEdit/src/document_model.scala
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