--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Wed May 21 15:24:42 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Wed May 21 16:21:11 2014 +0200
@@ -138,9 +138,8 @@
{
Swing_Thread.require {}
- private var zoom_factor = 100
-
- val pretty_text_area = new Pretty_Text_Area(view)
+ private val pretty_text_area = new Pretty_Text_Area(view)
+ private val zoom = new Font_Info.Zoom_Box { def changed = do_paint() }
size = new Dimension(500, 500)
contents = new BorderPanel {
@@ -170,7 +169,7 @@
{
Swing_Thread.later {
pretty_text_area.resize(
- Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
}
}
@@ -193,9 +192,6 @@
/* controls */
- private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
- zoom.tooltip = "Zoom factor for basic font size"
-
private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
pretty_text_area.search_label,
pretty_text_area.search_field,