# HG changeset patch
# User wenzelm
# Date 1442840170 -7200
# Node ID 46fa8f71e0edc852bba363370ef8aea80fe32086
# Parent  d5aeb401111a328eb55dbe5c20ced4a4ccc7ab9f
tuned;

diff -r d5aeb401111a -r 46fa8f71e0ed src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Mon Sep 21 13:53:35 2015 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Mon Sep 21 14:56:10 2015 +0200
@@ -21,6 +21,11 @@
 
 class Sledgehammer_Dockable(view: View, position: String) extends Dockable(view, position)
 {
+  GUI_Thread.require {}
+
+
+  /* text area */
+
   val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
@@ -51,7 +56,13 @@
 
   /* resize */
 
-  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+  private val delay_resize =
+    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
+
+  addComponentListener(new ComponentAdapter {
+    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+  })
 
   private def handle_resize()
   {
@@ -61,14 +72,6 @@
       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
   }
 
-  private val delay_resize =
-    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
-
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
-    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
-  })
-
 
   /* controls */
 
@@ -131,6 +134,8 @@
     reactions += { case ButtonClicked(_) => sledgehammer.locate_query() }
   }
 
+  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
       provers_label, Component.wrap(provers), isar_proofs, try0,