--- 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 }
}
--- 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()
}
--- 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{
--- 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)
--- 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)
--- 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 += {
--- 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))
}
}
--- 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,
--- 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,