src/Tools/jEdit/src/simplifier_trace_window.scala
changeset 57043 0f44d6dbd2a4
parent 57042 5576d22abf3c
child 57044 042d6e58cb40
     1.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 14:42:45 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 15:24:42 2014 +0200
     1.3 @@ -111,7 +111,8 @@
     1.4              {
     1.5                parent.parent match {
     1.6                  case None =>
     1.7 -                  Output.error_message("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
     1.8 +                  Output.error_message(
     1.9 +                    "Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
    1.10                  case Some(tree) =>
    1.11                    tree.children -= head.parent
    1.12                    walk_trace(tail, lookup)
    1.13 @@ -137,6 +138,8 @@
    1.14  {
    1.15    Swing_Thread.require {}
    1.16  
    1.17 +  private var zoom_factor = 100
    1.18 +
    1.19    val pretty_text_area = new Pretty_Text_Area(view)
    1.20  
    1.21    size = new Dimension(500, 500)
    1.22 @@ -166,7 +169,8 @@
    1.23    def do_paint()
    1.24    {
    1.25      Swing_Thread.later {
    1.26 -      pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
    1.27 +      pretty_text_area.resize(
    1.28 +        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    1.29      }
    1.30    }
    1.31  
    1.32 @@ -189,9 +193,13 @@
    1.33  
    1.34    /* controls */
    1.35  
    1.36 +  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
    1.37 +  zoom.tooltip = "Zoom factor for basic font size"
    1.38 +
    1.39    private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
    1.40      pretty_text_area.search_label,
    1.41 -    pretty_text_area.search_field)
    1.42 +    pretty_text_area.search_field,
    1.43 +    zoom)
    1.44  
    1.45    peer.add(controls.peer, BorderLayout.NORTH)
    1.46  }