# HG changeset patch # User wenzelm # Date 1274476767 -7200 # Node ID d014976dd69019e94244cd6d34819ec6cf224b1e # Parent 4a95a50d0ec483e369993f0cf1b0432575f62c0e tuned zoom_box; tuned tooltips; diff -r 4a95a50d0ec4 -r d014976dd690 src/Pure/library.scala --- a/src/Pure/library.scala Fri May 21 22:08:13 2010 +0200 +++ b/src/Pure/library.scala Fri May 21 23:19:27 2010 +0200 @@ -102,27 +102,27 @@ /* zoom box */ - def zoom_box(apply_factor: Int => Unit) = - new ComboBox( - List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) { - val Factor = "([0-9]+)%?"r - def reset(): Int = { selection.index = 3; 100 } + class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String]( + List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) + { + val Factor = "([0-9]+)%?"r + def parse(text: String): Int = + text match { + case Factor(s) => + val i = Integer.parseInt(s) + if (10 <= i && i <= 1000) i else 100 + case _ => 100 + } + def print(i: Int): String = i.toString + "%" - reactions += { - case SelectionChanged(_) => - val factor = - selection.item match { - case Factor(s) => - val i = Integer.parseInt(s) - if (10 <= i && i <= 1000) i else reset() - case _ => reset() - } - apply_factor(factor) - } - reset() - listenTo(selection) - makeEditable() + makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x)) + reactions += { + case SelectionChanged(_) => apply_factor(parse(selection.item)) } + listenTo(selection) + selection.index = 3 + prototypeDisplayValue = Some("00000%") + } /* timing */ diff -r 4a95a50d0ec4 -r d014976dd690 src/Tools/jEdit/src/jedit/output_dockable.scala --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Fri May 21 22:08:13 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Fri May 21 23:19:27 2010 +0200 @@ -34,27 +34,31 @@ /* controls */ - private val zoom = Library.zoom_box(factor => { zoom_factor = factor; handle_resize() }) + private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) zoom.tooltip = "Zoom factor for basic font size" private val update = new Button("Update") { reactions += { case ButtonClicked(_) => handle_update() } } - update.tooltip = "Update display according to state of command at caret position" + update.tooltip = + "Update display according to the
state of command at caret position" private val tracing = new CheckBox("Tracing") { reactions += { case ButtonClicked(_) => handle_update() } } - tracing.tooltip = "Indicate output of tracing messages" + tracing.tooltip = + "Indicate output of tracing messages
(also needs to be enabled on the prover side)" private val debug = new CheckBox("Debug") { reactions += { case ButtonClicked(_) => handle_update() } } - debug.tooltip = "Indicate output of debug messages (usually disabled on the prover side)" + debug.tooltip = + "Indicate output of debug messages
(also needs to be enabled on the prover side)" private val follow = new CheckBox("Follow") follow.selected = true - follow.tooltip = "Indicate automatic update according to caret movement or state changes" + follow.tooltip = + "Indicate automatic update following
caret movement or state changes" private def filtered_results(document: Document, cmd: Command): List[XML.Tree] = {