# HG changeset patch # User wenzelm # Date 1400683574 -7200 # Node ID d2fb95869d55f01fa0b2345dd02ba4fda1b81992 # Parent aceaca232177a66b1fa370eb8134bed0d8cfa9a5# Parent 042d6e58cb404fffde93e0b20d5e946fe0165dcb merged diff -r aceaca232177 -r d2fb95869d55 src/Pure/GUI/gui.scala --- 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 } } diff -r aceaca232177 -r d2fb95869d55 src/Tools/Graphview/src/graph_panel.scala --- 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() } diff -r aceaca232177 -r d2fb95869d55 src/Tools/Graphview/src/main_panel.scala --- 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{ diff -r aceaca232177 -r d2fb95869d55 src/Tools/jEdit/src/font_info.scala --- 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) diff -r aceaca232177 -r d2fb95869d55 src/Tools/jEdit/src/info_dockable.scala --- 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) diff -r aceaca232177 -r d2fb95869d55 src/Tools/jEdit/src/output_dockable.scala --- 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) } diff -r aceaca232177 -r d2fb95869d55 src/Tools/jEdit/src/pretty_text_area.scala --- 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) } diff -r aceaca232177 -r d2fb95869d55 src/Tools/jEdit/src/query_dockable.scala --- 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)) } } diff -r aceaca232177 -r d2fb95869d55 src/Tools/jEdit/src/simplifier_trace_window.scala --- 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) } diff -r aceaca232177 -r d2fb95869d55 src/Tools/jEdit/src/sledgehammer_dockable.scala --- 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,