1.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 23:19:28 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 23:20:01 2010 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4    val controls = new FlowPanel(FlowPanel.Alignment.Right)()
     1.5    add(controls.peer, BorderLayout.NORTH)
     1.6  
     1.7 -  val html_panel = new HTML_Panel(Isabelle.system, Isabelle.font_size(), null)
     1.8 +  val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()), null)
     1.9    add(html_panel, BorderLayout.CENTER)
    1.10  
    1.11  
    1.12 @@ -55,11 +55,20 @@
    1.13      }
    1.14    }
    1.15  
    1.16 +  private var zoom_factor = 100
    1.17 +
    1.18 +  private def handle_resize() =
    1.19 +    Swing_Thread.now {
    1.20 +      html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
    1.21 +    }
    1.22 +
    1.23 +  private val zoom = Library.zoom_box(factor => { zoom_factor = factor; handle_resize() })
    1.24 +
    1.25    private val update = new Button("Update") {
    1.26      reactions += { case ButtonClicked(_) => handle_update() }
    1.27    }
    1.28  
    1.29 -  val follow = new CheckBox("Follow")
    1.30 +  private val follow = new CheckBox("Follow")
    1.31    follow.selected = true
    1.32  
    1.33  
    1.34 @@ -68,7 +77,7 @@
    1.35    private val output_actor = actor {
    1.36      loop {
    1.37        react {
    1.38 -        case Session.Global_Settings => html_panel.resize(Isabelle.font_size())
    1.39 +        case Session.Global_Settings => handle_resize()
    1.40          case Render(body) => html_panel.render(body)
    1.41  
    1.42          case cmd: Command =>
    1.43 @@ -109,6 +118,6 @@
    1.44  
    1.45    /* init controls */
    1.46  
    1.47 -  controls.contents ++= List(update, follow)
    1.48 +  controls.contents ++= List(zoom, update, follow)
    1.49    handle_update()
    1.50  }

     2.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu May 20 23:19:28 2010 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu May 20 23:20:01 2010 +0200
     2.3 @@ -70,8 +70,9 @@
     2.4        jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
     2.5    }
     2.6  
     2.7 -  def font_size(): Int =
     2.8 -    (jEdit.getIntegerProperty("view.fontsize", 16) * Int_Property("relative-font-size", 100)) / 100
     2.9 +  def font_size(): Float =
    2.10 +    (jEdit.getIntegerProperty("view.fontsize", 16) *
    2.11 +      Int_Property("relative-font-size", 100)).toFloat / 100
    2.12  
    2.13  
    2.14    /* settings */