1 /* Title: Pure/library.scala
11 import java.lang.System
12 import java.awt.Component
13 import javax.swing.JOptionPane
15 import scala.swing.{ComboBox, TextArea, ScrollPane}
16 import scala.swing.event.SelectionChanged
17 import scala.collection.mutable
26 def apply(message: String): Throwable = new RuntimeException(message)
27 def unapply(exn: Throwable): Option[String] =
29 case e: RuntimeException => Some(Exn.message(e))
34 def error(message: String): Nothing = throw ERROR(message)
36 def cat_error(msg1: String, msg2: String): Nothing =
37 if (msg1 == "") error(msg1)
38 else error(msg1 + "\n" + msg2)
43 def separate[A](s: A, list: List[A]): List[A] =
45 case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs)
49 def space_explode(sep: Char, str: String): List[String] =
52 val result = new mutable.ListBuffer[String]
56 val i = str.indexOf(sep, start)
57 if (i == -1) { result += str.substring(start); finished = true }
58 else { result += str.substring(start, i); start = i + 1 }
63 def split_lines(str: String): List[String] = space_explode('\n', str)
65 def trim_line(str: String): String =
66 if (str.endsWith("\n")) str.substring(0, str.length - 1)
70 /* iterate over chunks (cf. space_explode) */
72 def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
74 private val end = source.length
75 private def next_chunk(i: Int): Option[(CharSequence, Int)] =
78 var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
79 Some((source.subSequence(i + 1, j), j))
83 private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
85 def hasNext(): Boolean = state.isDefined
86 def next(): CharSequence =
88 case Some((s, i)) => { state = next_chunk(i); s }
89 case None => Iterator.empty.next()
93 def first_line(source: CharSequence): String =
95 val lines = chunks(source)
96 if (lines.hasNext) lines.next.toString
103 def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
105 def quote(s: String): String = "\"" + s + "\""
106 def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
107 def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
110 /* reverse CharSequence */
112 class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
114 require(0 <= start && start <= end && end <= text.length)
116 def this(text: CharSequence) = this(text, 0, text.length)
118 def length: Int = end - start
119 def charAt(i: Int): Char = text.charAt(end - i - 1)
121 def subSequence(i: Int, j: Int): CharSequence =
122 if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
123 else throw new IndexOutOfBoundsException
125 override def toString: String =
127 val buf = new StringBuilder(length)
128 for (i <- 0 until length)
129 buf.append(charAt(i))
137 def scrollable_text(txt: String, width: Int = 80, editable: Boolean = false): ScrollPane =
139 val text = new TextArea(txt)
140 if (width > 0) text.columns = width
141 text.editable = editable
145 private def simple_dialog(kind: Int, default_title: String,
146 parent: Component, title: String, message: Seq[Any])
149 val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
150 JOptionPane.showMessageDialog(parent,
151 java_message.toArray.asInstanceOf[Array[AnyRef]],
152 if (title == null) default_title else title, kind)
156 def dialog(parent: Component, title: String, message: Any*) =
157 simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message)
159 def warning_dialog(parent: Component, title: String, message: Any*) =
160 simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message)
162 def error_dialog(parent: Component, title: String, message: Any*) =
163 simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message)
165 def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int =
167 val java_message = message map { case x: scala.swing.Component => x.peer case x => x }
168 JOptionPane.showConfirmDialog(parent,
169 java_message.toArray.asInstanceOf[Array[AnyRef]], title,
170 option_type, JOptionPane.QUESTION_MESSAGE)
176 class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
177 List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
179 val Factor = "([0-9]+)%?".r
180 def parse(text: String): Int =
183 val i = Integer.parseInt(s)
184 if (10 <= i && i <= 1000) i else 100
187 def print(i: Int): String = i.toString + "%"
189 makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
191 case SelectionChanged(_) => apply_factor(parse(selection.item))
195 prototypeDisplayValue = Some("00000%")
202 val ERROR = Library.ERROR
203 val error = Library.error _
204 val cat_error = Library.cat_error _
206 val space_explode = Library.space_explode _
207 val split_lines = Library.split_lines _
208 val cat_lines = Library.cat_lines _
209 val quote = Library.quote _
210 val commas = Library.commas _
211 val commas_quote = Library.commas_quote _