# 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] =
{