# HG changeset patch
# User wenzelm
# Date 1355148793 -3600
# Node ID 2af559170d0793aa4bb71df6b89b803ce60b5ae7
# Parent  358b6020f8b69b1b717d6060a4a06f170b8c4e0a
tuned;

diff -r 358b6020f8b6 -r 2af559170d07 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Mon Dec 10 13:52:33 2012 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Mon Dec 10 15:13:13 2012 +0100
@@ -36,7 +36,8 @@
     implicit_info = info
   }
 
-  private def reset_implicit(): Unit = set_implicit(Document.State.init.snapshot(), Nil)
+  private def reset_implicit(): Unit =
+    set_implicit(Document.State.init.snapshot(), Nil)
 
   def apply(view: View, snapshot: Document.Snapshot, info: XML.Body)
   {
@@ -81,6 +82,22 @@
   }
 
 
+  /* resize */
+
+  private val delay_resize =
+    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+
+  addComponentListener(new ComponentAdapter {
+    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+  })
+
+  private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
+  zoom.tooltip = "Zoom factor for basic font size"
+
+  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom)
+  add(controls.peer, BorderLayout.NORTH)
+
+
   /* main actor */
 
   private val main_actor = actor {
@@ -110,23 +127,4 @@
     PIDE.session.global_options -= main_actor
     delay_resize.revoke()
   }
-
-
-  /* resize */
-
-  private val delay_resize =
-    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
-
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
-  })
-
-
-  /* controls */
-
-  private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
-  zoom.tooltip = "Zoom factor for basic font size"
-
-  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom)
-  add(controls.peer, BorderLayout.NORTH)
 }