# HG changeset patch
# User wenzelm
# Date 1262120723 -3600
# Node ID 958634b374c0850932492a8089686d73f3e852fa
# Parent  9ad3431a34a531d0afd11e042ab55f7eeecf3f39
tuned;

diff -r 9ad3431a34a5 -r 958634b374c0 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Dec 29 21:54:54 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Dec 29 22:05:23 2009 +0100
@@ -142,11 +142,11 @@
   /* caret_listener */
 
   private var _selected_command: Command = null
-  def selected_command = _selected_command
-  def selected_command_=(state: Command)
+  private def selected_command = _selected_command
+  private def selected_command_=(cmd: Command)
   {
-    _selected_command = state
-    session.results.event(state)
+    _selected_command = cmd
+    session.results.event(cmd)
   }
 
   private val caret_listener = new CaretListener