# HG changeset patch
# User wenzelm
# Date 1274390401 -7200
# Node ID 8f747cee4e27f327865c7a79b61f0546c11c6c98
# Parent  39f4cce5a22cef40b3109fdd73b2c2e0c5d3a93d
zoom font size;

diff -r 39f4cce5a22c -r 8f747cee4e27 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 23:19:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 20 23:20:01 2010 +0200
@@ -31,7 +31,7 @@
   val controls = new FlowPanel(FlowPanel.Alignment.Right)()
   add(controls.peer, BorderLayout.NORTH)
 
-  val html_panel = new HTML_Panel(Isabelle.system, Isabelle.font_size(), null)
+  val html_panel = new HTML_Panel(Isabelle.system, scala.math.round(Isabelle.font_size()), null)
   add(html_panel, BorderLayout.CENTER)
 
 
@@ -55,11 +55,20 @@
     }
   }
 
+  private var zoom_factor = 100
+
+  private def handle_resize() =
+    Swing_Thread.now {
+      html_panel.resize(scala.math.round(Isabelle.font_size() * zoom_factor / 100))
+    }
+
+  private val zoom = Library.zoom_box(factor => { zoom_factor = factor; handle_resize() })
+
   private val update = new Button("Update") {
     reactions += { case ButtonClicked(_) => handle_update() }
   }
 
-  val follow = new CheckBox("Follow")
+  private val follow = new CheckBox("Follow")
   follow.selected = true
 
 
@@ -68,7 +77,7 @@
   private val output_actor = actor {
     loop {
       react {
-        case Session.Global_Settings => html_panel.resize(Isabelle.font_size())
+        case Session.Global_Settings => handle_resize()
         case Render(body) => html_panel.render(body)
 
         case cmd: Command =>
@@ -109,6 +118,6 @@
 
   /* init controls */
 
-  controls.contents ++= List(update, follow)
+  controls.contents ++= List(zoom, update, follow)
   handle_update()
 }
diff -r 39f4cce5a22c -r 8f747cee4e27 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu May 20 23:19:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu May 20 23:20:01 2010 +0200
@@ -70,8 +70,9 @@
       jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
   }
 
-  def font_size(): Int =
-    (jEdit.getIntegerProperty("view.fontsize", 16) * Int_Property("relative-font-size", 100)) / 100
+  def font_size(): Float =
+    (jEdit.getIntegerProperty("view.fontsize", 16) *
+      Int_Property("relative-font-size", 100)).toFloat / 100
 
 
   /* settings */