src/Tools/jEdit/src/simplifier_trace_window.scala
changeset 57044 042d6e58cb40
parent 57043 0f44d6dbd2a4
child 57612 990ffb84489b
     1.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 15:24:42 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 16:21:11 2014 +0200
     1.3 @@ -138,9 +138,8 @@
     1.4  {
     1.5    Swing_Thread.require {}
     1.6  
     1.7 -  private var zoom_factor = 100
     1.8 -
     1.9 -  val pretty_text_area = new Pretty_Text_Area(view)
    1.10 +  private val pretty_text_area = new Pretty_Text_Area(view)
    1.11 +  private val zoom = new Font_Info.Zoom_Box { def changed = do_paint() }
    1.12  
    1.13    size = new Dimension(500, 500)
    1.14    contents = new BorderPanel {
    1.15 @@ -170,7 +169,7 @@
    1.16    {
    1.17      Swing_Thread.later {
    1.18        pretty_text_area.resize(
    1.19 -        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    1.20 +        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
    1.21      }
    1.22    }
    1.23  
    1.24 @@ -193,9 +192,6 @@
    1.25  
    1.26    /* controls */
    1.27  
    1.28 -  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
    1.29 -  zoom.tooltip = "Zoom factor for basic font size"
    1.30 -
    1.31    private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
    1.32      pretty_text_area.search_label,
    1.33      pretty_text_area.search_field,