--- a/src/Pure/GUI/gui.scala Wed May 21 16:26:04 2014 +0200
+++ b/src/Pure/GUI/gui.scala Wed May 21 16:46:14 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 16:26:04 2014 +0200
+++ b/src/Tools/Graphview/src/graph_panel.scala Wed May 21 16:46:14 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 16:26:04 2014 +0200
+++ b/src/Tools/Graphview/src/main_panel.scala Wed May 21 16:46:14 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 16:26:04 2014 +0200
+++ b/src/Tools/jEdit/src/font_info.scala Wed May 21 16:46:14 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 16:26:04 2014 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Wed May 21 16:46:14 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,11 +88,8 @@
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_pattern, zoom)
+ 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 16:26:04 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Wed May 21 16:46:14 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 += {
@@ -144,6 +141,6 @@
private val controls =
new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update,
- pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
+ pretty_text_area.search_label, pretty_text_area.search_field, zoom)
add(controls.peer, BorderLayout.NORTH)
}
--- a/src/Tools/jEdit/src/pretty_text_area.scala Wed May 21 16:26:04 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed May 21 16:46:14 2014 +0200
@@ -187,7 +187,7 @@
tooltip = "Search and highlight output via regular expression"
}
- val search_pattern: Component =
+ val search_field: Component =
Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search")
{
private val input_delay =
@@ -204,7 +204,7 @@
setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
})
- private val search_pattern_foreground = search_pattern.foreground
+ private val search_field_foreground = search_field.foreground
private def search_action(text_field: JTextField)
{
@@ -220,7 +220,7 @@
text_area.getPainter.repaint()
}
text_field.setForeground(
- if (ok) search_pattern_foreground else current_rendering.error_color)
+ if (ok) search_field_foreground else current_rendering.error_color)
}
--- a/src/Tools/jEdit/src/query_dockable.scala Wed May 21 16:26:04 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Wed May 21 16:46:14 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)
@@ -125,7 +120,7 @@
new Wrap_Panel(Wrap_Panel.Alignment.Right)(
query_label, Component.wrap(query), limit, allow_dups,
process_indicator.component, apply_button,
- pretty_text_area.search_label, pretty_text_area.search_pattern)
+ pretty_text_area.search_label, pretty_text_area.search_field)
def select { control_panel.contents += zoom }
@@ -173,7 +168,7 @@
private val control_panel =
new Wrap_Panel(Wrap_Panel.Alignment.Right)(
query_label, Component.wrap(query), process_indicator.component, apply_button,
- pretty_text_area.search_label, pretty_text_area.search_pattern)
+ pretty_text_area.search_label, pretty_text_area.search_field)
def select { control_panel.contents += zoom }
@@ -268,7 +263,7 @@
control_panel.contents.clear
control_panel.contents ++=
List(query_label, selector, process_indicator.component, apply_button,
- pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
+ pretty_text_area.search_label, pretty_text_area.search_field, zoom)
}
val page =
@@ -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 16:26:04 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Wed May 21 16:46:14 2014 +0200
@@ -111,7 +111,8 @@
{
parent.parent match {
case None =>
- Output.error_message("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
+ Output.error_message(
+ "Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
case Some(tree) =>
tree.children -= head.parent
walk_trace(tail, lookup)
@@ -137,7 +138,8 @@
{
Swing_Thread.require {}
- 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 {
@@ -166,7 +168,8 @@
def do_paint()
{
Swing_Thread.later {
- pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_font_scale")))
+ pretty_text_area.resize(
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
}
}
@@ -191,7 +194,8 @@
private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
pretty_text_area.search_label,
- pretty_text_area.search_pattern)
+ pretty_text_area.search_field,
+ zoom)
peer.add(controls.peer, BorderLayout.NORTH)
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed May 21 16:26:04 2014 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed May 21 16:46:14 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,