src/Tools/jEdit/src/simplifier_trace_window.scala

 class Simplifier_Trace_Window(
   view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
 {
   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 {
     layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
   }

 
   def do_paint()
   {
     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))
     }
   }
 
   def handle_resize()
   {

   })
 
 
   /* 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,
     zoom)