# HG changeset patch
# User wenzelm
# Date 1442828703 -7200
# Node ID c0a5ebecc68b447171697abf2cf53cb025d36774
# Parent  94efa2688ff6b8c9b52df0e61f02f6dd5011957a
tuned;

diff -r 94efa2688ff6 -r c0a5ebecc68b src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sat Sep 19 22:32:26 2015 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Sep 21 11:45:03 2015 +0200
@@ -37,8 +37,6 @@
   override def detach_operation = pretty_text_area.detach_operation
 
 
-  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
-
   private def handle_resize()
   {
     GUI_Thread.require {}
@@ -83,6 +81,28 @@
   }
 
 
+  /* controls */
+
+  private val auto_update = new CheckBox("Auto update") {
+    tooltip = "Indicate automatic update following cursor movement"
+    reactions += {
+      case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
+    selected = do_update
+  }
+
+  private val update = new Button("Update") {
+    tooltip = "Update display according to the command at cursor position"
+    reactions += { case ButtonClicked(_) => handle_update(true, None) }
+  }
+
+  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+
+  private val controls =
+    new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update,
+      pretty_text_area.search_label, pretty_text_area.search_field, zoom)
+  add(controls.peer, BorderLayout.NORTH)
+
+
   /* main */
 
   private val main =
@@ -124,24 +144,4 @@
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
     override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
   })
-
-
-  /* controls */
-
-  private val auto_update = new CheckBox("Auto update") {
-    tooltip = "Indicate automatic update following cursor movement"
-    reactions += {
-      case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
-    selected = do_update
-  }
-
-  private val update = new Button("Update") {
-    tooltip = "Update display according to the command at cursor position"
-    reactions += { case ButtonClicked(_) => handle_update(true, None) }
-  }
-
-  private val controls =
-    new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update,
-      pretty_text_area.search_label, pretty_text_area.search_field, zoom)
-  add(controls.peer, BorderLayout.NORTH)
 }