# HG changeset patch
# User wenzelm
# Date 1442860303 -7200
# Node ID f9aaca00be49986f2f955fb54dad0b620aff32c5
# Parent  04c769fe1cb540d0f20f08e811a8240b8168b004
removed auto update -- bad reactivity;

diff -r 04c769fe1cb5 -r f9aaca00be49 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Mon Sep 21 20:21:29 2015 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala	Mon Sep 21 20:31:43 2015 +0200
@@ -57,10 +57,6 @@
 
   /* update */
 
-  private var do_update = true
-
-  private def maybe_update(): Unit = GUI_Thread.require { if (do_update) update() }
-
   def update()
   {
     GUI_Thread.require {}
@@ -78,12 +74,6 @@
 
   /* controls */
 
-  private val auto_update_button = new CheckBox("Auto update") {
-    tooltip = "Indicate automatic update following cursor movement"
-    reactions += { case ButtonClicked(_) => do_update = this.selected; maybe_update() }
-    selected = do_update
-  }
-
   private val update_button = new Button("Update") {
     tooltip = "Update display according to the command at cursor position"
     reactions += { case ButtonClicked(_) => print_state.apply_query(Nil) }
@@ -97,7 +87,7 @@
   private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
 
   private val controls =
-    new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update_button, update_button, locate_button,
+    new Wrap_Panel(Wrap_Panel.Alignment.Right)(update_button, locate_button,
       pretty_text_area.search_label, pretty_text_area.search_field, zoom)
   add(controls.peer, BorderLayout.NORTH)
 
@@ -110,30 +100,19 @@
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
         GUI_Thread.later { handle_resize() }
-
-      case changed: Session.Commands_Changed =>
-        if (changed.assignment) GUI_Thread.later { maybe_update() }
-
-      case Session.Caret_Focus =>
-        GUI_Thread.later { maybe_update() }
     }
 
   override def init()
   {
     PIDE.session.global_options += main
-    PIDE.session.commands_changed += main
-    PIDE.session.caret_focus += main
     handle_resize()
     print_state.activate()
-    maybe_update()
   }
 
   override def exit()
   {
     print_state.deactivate()
-    PIDE.session.caret_focus -= main
     PIDE.session.global_options -= main
-    PIDE.session.commands_changed -= main
     delay_resize.revoke()
   }
 }