1 /* Title: Pure/library.scala
10 import java.lang.System
11 import java.awt.Component
12 import javax.swing.JOptionPane
14 import scala.swing.ComboBox
15 import scala.swing.event.SelectionChanged
20 /* partial functions */
22 def undefined[A, B] = new PartialFunction[A, B] {
23 def apply(x: A): B = throw new NoSuchElementException("undefined")
24 def isDefinedAt(x: A) = false
30 def separate[A](s: A, list: List[A]): List[A] =
32 case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs)
37 /* reverse CharSequence */
39 class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
41 require(0 <= start && start <= end && end <= text.length)
43 def this(text: CharSequence) = this(text, 0, text.length)
45 def length: Int = end - start
46 def charAt(i: Int): Char = text.charAt(end - i - 1)
48 def subSequence(i: Int, j: Int): CharSequence =
49 if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
50 else throw new IndexOutOfBoundsException
52 override def toString: String =
54 val buf = new StringBuilder(length)
55 for (i <- 0 until length)
62 /* iterate over chunks (cf. space_explode/split_lines in ML) */
64 def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
66 private val end = source.length
67 private def next_chunk(i: Int): Option[(CharSequence, Int)] =
70 var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
71 Some((source.subSequence(i + 1, j), j))
75 private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
77 def hasNext(): Boolean = state.isDefined
78 def next(): CharSequence =
80 case Some((s, i)) => { state = next_chunk(i); s }
81 case None => Iterator.empty.next()
88 private def simple_dialog(kind: Int, default_title: String)
89 (parent: Component, title: String, message: Any*)
92 val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
93 JOptionPane.showMessageDialog(parent,
94 java_message.toArray.asInstanceOf[Array[AnyRef]],
95 if (title == null) default_title else title, kind)
99 def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _
100 def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
101 def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
106 class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
107 List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
109 val Factor = "([0-9]+)%?"r
110 def parse(text: String): Int =
113 val i = Integer.parseInt(s)
114 if (10 <= i && i <= 1000) i else 100
117 def print(i: Int): String = i.toString + "%"
119 makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
121 case SelectionChanged(_) => apply_factor(parse(selection.item))
125 prototypeDisplayValue = Some("00000%")
131 def timeit[A](message: String)(e: => A) =
133 val start = System.nanoTime()
134 val result = Exn.capture(e)
135 val stop = System.nanoTime()
137 (if (message == null || message.isEmpty) "" else message + ": ") +
138 ((stop - start).toDouble / 1000000) + "ms elapsed time")