1.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Dec 29 21:54:54 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Dec 29 22:05:23 2009 +0100
     1.3 @@ -142,11 +142,11 @@
     1.4    /* caret_listener */
     1.5  
     1.6    private var _selected_command: Command = null
     1.7 -  def selected_command = _selected_command
     1.8 -  def selected_command_=(state: Command)
     1.9 +  private def selected_command = _selected_command
    1.10 +  private def selected_command_=(cmd: Command)
    1.11    {
    1.12 -    _selected_command = state
    1.13 -    session.results.event(state)
    1.14 +    _selected_command = cmd
    1.15 +    session.results.event(cmd)
    1.16    }
    1.17  
    1.18    private val caret_listener = new CaretListener