# HG changeset patch
# User wenzelm
# Date 1262120094 -3600
# Node ID 9ad3431a34a531d0afd11e042ab55f7eeecf3f39
# Parent  0fed930f29927de30037ce3bc1dfca79c13632cf
tuned caret_listener/selected_command;

diff -r 0fed930f2992 -r 9ad3431a34a5 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Dec 29 21:31:17 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Dec 29 21:54:54 2009 +0100
@@ -139,6 +139,31 @@
   }
 
 
+  /* caret_listener */
+
+  private var _selected_command: Command = null
+  def selected_command = _selected_command
+  def selected_command_=(state: Command)
+  {
+    _selected_command = state
+    session.results.event(state)
+  }
+
+  private val caret_listener = new CaretListener
+  {
+    override def caretUpdate(e: CaretEvent) {
+      val doc = model.current_document()
+      doc.command_at(e.getDot) match {
+        case Some(cmd)
+          if (doc.token_start(cmd.tokens.first) <= e.getDot &&
+            selected_command != cmd) =>
+          selected_command = cmd  // FIXME !?
+        case _ =>
+      }
+    }
+  }
+
+
   /* (re)painting */
 
   private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }
@@ -156,8 +181,8 @@
     val (start, stop) = model.lines_of_command(cmd)
     text_area.invalidateLineRange(start, stop)
 
-    if (Isabelle.session.selected_state == cmd)
-      Isabelle.session.selected_state = cmd
+    if (selected_command == cmd)
+      selected_command = cmd
   }
 
   private def invalidate_all() =
@@ -245,29 +270,14 @@
   }
 
 
-  private val selected_state_controller = new CaretListener
-  {
-    override def caretUpdate(e: CaretEvent) {
-      val doc = model.current_document()
-      doc.command_at(e.getDot) match {
-        case Some(cmd)
-          if (doc.token_start(cmd.tokens.first) <= e.getDot &&
-            Isabelle.session.selected_state != cmd) =>
-          Isabelle.session.selected_state = cmd  // FIXME !?
-        case _ =>
-      }
-    }
-  }
-
-
   /* activation */
 
   private def activate()
   {
-    text_area.addCaretListener(selected_state_controller)
-    text_area.addLeftOfScrollBar(overview)
     text_area.getPainter.
       addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
+    text_area.addCaretListener(caret_listener)
+    text_area.addLeftOfScrollBar(overview)
     session.command_change += command_change_actor
   }
 
@@ -275,8 +285,8 @@
   {
     session.command_change -= command_change_actor
     command_change_actor !? Exit
+    text_area.removeLeftOfScrollBar(overview)
+    text_area.removeCaretListener(caret_listener)
     text_area.getPainter.removeExtension(text_area_extension)
-    text_area.removeLeftOfScrollBar(overview)
-    text_area.removeCaretListener(selected_state_controller)
   }
 }
\ No newline at end of file
diff -r 0fed930f2992 -r 9ad3431a34a5 src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Tue Dec 29 21:31:17 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Tue Dec 29 21:54:54 2009 +0100
@@ -33,7 +33,7 @@
   def create_id(): String = synchronized { id_count += 1; "j" + id_count }
 
 
-  /* document state information -- vars belong to session_actor */
+  /* document state information -- owned by session_actor */
 
   @volatile private var outer_syntax = new Outer_Syntax(system.symbols)
   def syntax(): Outer_Syntax = outer_syntax
@@ -184,11 +184,4 @@
 
   def begin_document(path: String): Proof_Document =
     (session_actor !? Begin_Document(path)).asInstanceOf[Proof_Document]
-
-
-  /* selected state */  // FIXME eliminate!?!
-
-  private var _selected_state: Command = null
-  def selected_state = _selected_state
-  def selected_state_=(state: Command) { _selected_state = state; results.event(state) }
 }