src/Tools/jEdit/src/output_dockable.scala

   val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
   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 {}
 

     current_results = new_results
     current_output = new_output
   }
 
 
+  /* 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 =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>

 
   addComponentListener(new ComponentAdapter {
     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)
 }