# HG changeset patch
# User wenzelm
# Date 1308768978 -7200
# Node ID 270ce5ff20865bf436b818a8250ba3a9e24ac068
# Parent  d138e7482a1bd7f66b7a3380f649527fbe996a7c
clarified init/exit procedure;

diff -r d138e7482a1b -r 270ce5ff2086 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()
   }
 }