src/Pure/library.scala
author wenzelm
Thu Dec 31 23:47:09 2009 +0100 (2009-12-31 ago)
changeset 34216 ada8eb23a08e
parent 34198 ff5486262cd6
child 34314 f799f3749596
permissions -rw-r--r--
added simple dialogs;
wenzelm@34136
     1
/*  Title:      Pure/library.scala
wenzelm@34136
     2
    Author:     Makarius
wenzelm@34136
     3
wenzelm@34136
     4
Basic library.
wenzelm@34136
     5
*/
wenzelm@34136
     6
wenzelm@34136
     7
package isabelle
wenzelm@34136
     8
wenzelm@34136
     9
import java.lang.System
wenzelm@34216
    10
import java.awt.Component
wenzelm@34216
    11
import javax.swing.JOptionPane
wenzelm@34136
    12
wenzelm@34136
    13
wenzelm@34136
    14
object Library
wenzelm@34136
    15
{
wenzelm@34141
    16
  /* reverse CharSequence */
wenzelm@34141
    17
wenzelm@34141
    18
  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
wenzelm@34141
    19
  {
wenzelm@34141
    20
    require(0 <= start && start <= end && end <= text.length)
wenzelm@34141
    21
wenzelm@34141
    22
    def this(text: CharSequence) = this(text, 0, text.length)
wenzelm@34141
    23
wenzelm@34141
    24
    def length: Int = end - start
wenzelm@34141
    25
    def charAt(i: Int): Char = text.charAt(end - i - 1)
wenzelm@34141
    26
wenzelm@34141
    27
    def subSequence(i: Int, j: Int): CharSequence =
wenzelm@34141
    28
      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
wenzelm@34141
    29
      else throw new IndexOutOfBoundsException
wenzelm@34141
    30
wenzelm@34141
    31
    override def toString: String =
wenzelm@34141
    32
    {
wenzelm@34141
    33
      val buf = new StringBuilder(length)
wenzelm@34141
    34
      for (i <- 0 until length)
wenzelm@34141
    35
        buf.append(charAt(i))
wenzelm@34141
    36
      buf.toString
wenzelm@34141
    37
    }
wenzelm@34141
    38
  }
wenzelm@34141
    39
wenzelm@34141
    40
wenzelm@34216
    41
  /* simple dialogs */
wenzelm@34216
    42
wenzelm@34216
    43
  private def simple_dialog(kind: Int, default_title: String)
wenzelm@34216
    44
    (parent: Component, title: String, message: Any*)
wenzelm@34216
    45
  {
wenzelm@34216
    46
    JOptionPane.showMessageDialog(parent,
wenzelm@34216
    47
      message.toArray.asInstanceOf[Array[AnyRef]],
wenzelm@34216
    48
      if (title == null) default_title else title, kind)
wenzelm@34216
    49
  }
wenzelm@34216
    50
wenzelm@34216
    51
  def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _
wenzelm@34216
    52
  def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
wenzelm@34216
    53
  def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
wenzelm@34216
    54
wenzelm@34216
    55
wenzelm@34136
    56
  /* timing */
wenzelm@34136
    57
wenzelm@34136
    58
  def timeit[A](e: => A) =
wenzelm@34136
    59
  {
wenzelm@34136
    60
    val start = System.currentTimeMillis()
wenzelm@34136
    61
    val result = Exn.capture(e)
wenzelm@34136
    62
    val stop = System.currentTimeMillis()
wenzelm@34136
    63
    System.err.println((stop - start) + "ms elapsed time")
wenzelm@34136
    64
    Exn.release(result)
wenzelm@34136
    65
  }
wenzelm@34136
    66
}