src/Tools/jEdit/src/document_view.scala
changeset 44805 48a5c104d434
parent 44776 47e8c8daccae
child 45460 dcd02d1a25d7
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Sep 07 21:31:50 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Sep 07 21:38:48 2011 +0200
     1.3 @@ -362,7 +362,7 @@
     1.4  
     1.5    private val caret_listener = new CaretListener {
     1.6      private val delay = Swing_Thread.delay_last(session.input_delay) {
     1.7 -      session.perspective.event(Session.Perspective)
     1.8 +      session.caret_focus.event(Session.Caret_Focus)
     1.9      }
    1.10      override def caretUpdate(e: CaretEvent) { delay() }
    1.11    }