# HG changeset patch
# User wenzelm
# Date 1400678682 -7200
# Node ID 0f44d6dbd2a4a8c008f2197f17e67cf4e98224bc
# Parent  5576d22abf3cb998f442d70f7a12e6194904fe3f
added zoom box, like for outer output windows;

diff -r 5576d22abf3c -r 0f44d6dbd2a4 src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 14:42:45 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 15:24:42 2014 +0200
@@ -111,7 +111,8 @@
             {
               parent.parent match {
                 case None =>
-                  Output.error_message("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
+                  Output.error_message(
+                    "Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
                 case Some(tree) =>
                   tree.children -= head.parent
                   walk_trace(tail, lookup)
@@ -137,6 +138,8 @@
 {
   Swing_Thread.require {}
 
+  private var zoom_factor = 100
+
   val pretty_text_area = new Pretty_Text_Area(view)
 
   size = new Dimension(500, 500)
@@ -166,7 +169,8 @@
   def do_paint()
   {
     Swing_Thread.later {
-      pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
+      pretty_text_area.resize(
+        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
     }
   }
 
@@ -189,9 +193,13 @@
 
   /* 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)
+    pretty_text_area.search_field,
+    zoom)
 
   peer.add(controls.peer, BorderLayout.NORTH)
 }