src/Tools/jEdit/src/document_model.scala

--- a/src/Tools/jEdit/src/document_model.scala	Wed Jun 22 20:38:03 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Jun 22 20:56:18 2011 +0200
@@ -131,16 +131,17 @@
 
   /* activation */
 
-  def activate()
+  private def activate()
   {
     buffer.addBufferListener(buffer_listener)
+    pending_edits.init()
     buffer.propertiesChanged()
-    pending_edits.init()
   }
 
-  def deactivate()
+  private def deactivate()
   {
     pending_edits.flush()
     buffer.removeBufferListener(buffer_listener)
+    buffer.propertiesChanged()
   }
 }