--- 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