tuned;
authorwenzelm
Tue, 29 Dec 2009 22:05:23 +0100
changeset 34811 958634b374c0
parent 34810 9ad3431a34a5
child 34812 4c875ed8b248
tuned;
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