# HG changeset patch
# User wenzelm
# Date 1400682071 -7200
# Node ID 042d6e58cb404fffde93e0b20d5e946fe0165dcb
# Parent  0f44d6dbd2a4a8c008f2197f17e67cf4e98224bc
more uniform Font_Info.Zoom_Box;
misc tuning and clarification;

diff -r 0f44d6dbd2a4 -r 042d6e58cb40 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Wed May 21 15:24:42 2014 +0200
+++ b/src/Pure/GUI/gui.scala	Wed May 21 16:21:11 2014 +0200
@@ -117,19 +117,23 @@
 
   /* zoom box */
 
-  class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
+  private val Zoom_Factor = "([0-9]+)%?".r
+
+  abstract class Zoom_Box extends ComboBox[String](
     List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
   {
-    val Factor = "([0-9]+)%?".r
-    def parse(text: String): Int =
+    def changed: Unit
+    def factor: Int = parse(selection.item)
+
+    private def parse(text: String): Int =
       text match {
-        case Factor(s) =>
+        case Zoom_Factor(s) =>
           val i = Integer.parseInt(s)
           if (10 <= i && i < 1000) i else 100
         case _ => 100
       }
 
-    def print(i: Int): String = i.toString + "%"
+    private def print(i: Int): String = i.toString + "%"
 
     def set_item(i: Int) {
       peer.getEditor match {
@@ -144,11 +148,10 @@
       case _ =>
     }
 
-    reactions += {
-      case SelectionChanged(_) => apply_factor(parse(selection.item))
-    }
+    selection.index = 3
+
     listenTo(selection)
-    selection.index = 3
+    reactions += { case SelectionChanged(_) => changed }
   }
 
 
diff -r 0f44d6dbd2a4 -r 042d6e58cb40 src/Tools/Graphview/src/graph_panel.scala
--- a/src/Tools/Graphview/src/graph_panel.scala	Wed May 21 15:24:42 2014 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala	Wed May 21 16:21:11 2014 +0200
@@ -63,12 +63,12 @@
     refresh()
   }
 
-  val zoom_box: GUI.Zoom_Box = new GUI.Zoom_Box(percent => rescale(0.01 * percent))
+  val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) }
 
   def rescale(s: Double)
   {
     Transform.scale = s
-    if (zoom_box != null) zoom_box.set_item((Transform.scale_discrete * 100).round.toInt)
+    if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).round.toInt)
     refresh()
   }
 
diff -r 0f44d6dbd2a4 -r 042d6e58cb40 src/Tools/Graphview/src/main_panel.scala
--- a/src/Tools/Graphview/src/main_panel.scala	Wed May 21 15:24:42 2014 +0200
+++ b/src/Tools/Graphview/src/main_panel.scala	Wed May 21 16:21:11 2014 +0200
@@ -67,7 +67,7 @@
       }
     }
     contents += Swing.RigidBox(new Dimension(10, 0))
-    contents += graph_panel.zoom_box
+    contents += graph_panel.zoom
 
     contents += Swing.RigidBox(new Dimension(10, 0))
     contents += new Button{
diff -r 0f44d6dbd2a4 -r 042d6e58cb40 src/Tools/jEdit/src/font_info.scala
--- a/src/Tools/jEdit/src/font_info.scala	Wed May 21 15:24:42 2014 +0200
+++ b/src/Tools/jEdit/src/font_info.scala	Wed May 21 16:21:11 2014 +0200
@@ -85,6 +85,11 @@
       change_size(_ => size)
     }
   }
+
+
+  /* zoom box */
+
+  abstract class Zoom_Box extends GUI.Zoom_Box { tooltip = "Zoom factor for output font size" }
 }
 
 sealed case class Font_Info(family: String, size: Float)
diff -r 0f44d6dbd2a4 -r 042d6e58cb40 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Wed May 21 15:24:42 2014 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Wed May 21 16:21:11 2014 +0200
@@ -50,8 +50,6 @@
 {
   /* component state -- owned by Swing thread */
 
-  private var zoom_factor = 100
-
   private val snapshot = Info_Dockable.implicit_snapshot
   private val results = Info_Dockable.implicit_results
   private val info = Info_Dockable.implicit_info
@@ -70,12 +68,14 @@
 
   pretty_text_area.update(snapshot, results, info)
 
+  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+
   private def handle_resize()
   {
     Swing_Thread.require {}
 
     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))
   }
 
 
@@ -88,9 +88,6 @@
     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   })
 
-  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)
   add(controls.peer, BorderLayout.NORTH)
diff -r 0f44d6dbd2a4 -r 042d6e58cb40 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Wed May 21 15:24:42 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed May 21 16:21:11 2014 +0200
@@ -22,7 +22,6 @@
 {
   /* component state -- owned by Swing thread */
 
-  private var zoom_factor = 100
   private var do_update = true
   private var current_snapshot = Document.Snapshot.init
   private var current_command = Command.empty
@@ -38,12 +37,14 @@
   override def detach_operation = pretty_text_area.detach_operation
 
 
+  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+
   private def handle_resize()
   {
     Swing_Thread.require {}
 
     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))
   }
 
   private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
@@ -126,10 +127,6 @@
 
   /* controls */
 
-  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
-    tooltip = "Zoom factor for output font size"
-  }
-
   private val auto_update = new CheckBox("Auto update") {
     tooltip = "Indicate automatic update following cursor movement"
     reactions += {
diff -r 0f44d6dbd2a4 -r 042d6e58cb40 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Wed May 21 15:24:42 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Wed May 21 16:21:11 2014 +0200
@@ -35,12 +35,7 @@
 {
   /* common GUI components */
 
-  private var zoom_factor = 100
-  private val zoom =
-    new GUI.Zoom_Box(factor => if (zoom_factor != factor) { zoom_factor = factor; handle_resize() })
-    {
-      tooltip = "Zoom factor for output font size"
-    }
+  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
 
   private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
     new Completion_Popup.History_Text_Field(property)
@@ -317,7 +312,7 @@
     Swing_Thread.require {
       for (op <- operations) {
         op.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))
       }
     }
 
diff -r 0f44d6dbd2a4 -r 042d6e58cb40 src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 15:24:42 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 16:21:11 2014 +0200
@@ -138,9 +138,8 @@
 {
   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 {
@@ -170,7 +169,7 @@
   {
     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))
     }
   }
 
@@ -193,9 +192,6 @@
 
   /* 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,
diff -r 0f44d6dbd2a4 -r 042d6e58cb40 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed May 21 15:24:42 2014 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed May 21 16:21:11 2014 +0200
@@ -51,14 +51,14 @@
 
   /* resize */
 
-  private var zoom_factor = 100
+  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
 
   private def handle_resize()
   {
     Swing_Thread.require {}
 
     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))
   }
 
   private val delay_resize =
@@ -122,10 +122,6 @@
     reactions += { case ButtonClicked(_) => sledgehammer.locate_query() }
   }
 
-  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
-    tooltip = "Zoom factor for output font size"
-  }
-
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
       provers_label, Component.wrap(provers), isar_proofs,