--- 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 */
--- 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 =
+ "<html>Update display according to the<br>state of command at caret position</html>"
private val tracing = new CheckBox("Tracing") {
reactions += { case ButtonClicked(_) => handle_update() }
}
- tracing.tooltip = "Indicate output of tracing messages"
+ tracing.tooltip =
+ "<html>Indicate output of tracing messages<br>(also needs to be enabled on the prover side)</html>"
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 =
+ "<html>Indicate output of debug messages<br>(also needs to be enabled on the prover side)</html>"
private val follow = new CheckBox("Follow")
follow.selected = true
- follow.tooltip = "Indicate automatic update according to caret movement or state changes"
+ follow.tooltip =
+ "<html>Indicate automatic update following<br>caret movement or state changes</html>"
private def filtered_results(document: Document, cmd: Command): List[XML.Tree] =
{