--- 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,