src/Pure/library.scala
author wenzelm
Mon May 10 23:46:49 2010 +0200 (2010-05-10 ago)
changeset 36791 b8384c455b40
parent 36688 321d392ab12e
child 37018 39f4cce5a22c
permissions -rw-r--r--
simple dialogs: ensure Swing thread;
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@36688
    16
  /* separate */
wenzelm@36688
    17
wenzelm@36688
    18
  def separate[A](s: A, list: List[A]): List[A] =
wenzelm@36688
    19
    list match {
wenzelm@36688
    20
      case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs)
wenzelm@36688
    21
      case _ => list
wenzelm@36688
    22
    }
wenzelm@36688
    23
wenzelm@36688
    24
wenzelm@34141
    25
  /* reverse CharSequence */
wenzelm@34141
    26
wenzelm@34141
    27
  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
wenzelm@34141
    28
  {
wenzelm@34141
    29
    require(0 <= start && start <= end && end <= text.length)
wenzelm@34141
    30
wenzelm@34141
    31
    def this(text: CharSequence) = this(text, 0, text.length)
wenzelm@34141
    32
wenzelm@34141
    33
    def length: Int = end - start
wenzelm@34141
    34
    def charAt(i: Int): Char = text.charAt(end - i - 1)
wenzelm@34141
    35
wenzelm@34141
    36
    def subSequence(i: Int, j: Int): CharSequence =
wenzelm@34141
    37
      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
wenzelm@34141
    38
      else throw new IndexOutOfBoundsException
wenzelm@34141
    39
wenzelm@34141
    40
    override def toString: String =
wenzelm@34141
    41
    {
wenzelm@34141
    42
      val buf = new StringBuilder(length)
wenzelm@34141
    43
      for (i <- 0 until length)
wenzelm@34141
    44
        buf.append(charAt(i))
wenzelm@34141
    45
      buf.toString
wenzelm@34141
    46
    }
wenzelm@34141
    47
  }
wenzelm@34141
    48
wenzelm@34141
    49
wenzelm@36685
    50
  /* iterate over chunks (cf. space_explode/split_lines in ML) */
wenzelm@36685
    51
wenzelm@36685
    52
  def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
wenzelm@36685
    53
  {
wenzelm@36685
    54
    private val end = source.length
wenzelm@36685
    55
    private def next_chunk(i: Int): Option[(CharSequence, Int)] =
wenzelm@36685
    56
    {
wenzelm@36685
    57
      if (i < end) {
wenzelm@36685
    58
        var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
wenzelm@36685
    59
        Some((source.subSequence(i + 1, j), j))
wenzelm@36685
    60
      }
wenzelm@36685
    61
      else None
wenzelm@36685
    62
    }
wenzelm@36685
    63
    private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
wenzelm@36685
    64
wenzelm@36685
    65
    def hasNext(): Boolean = state.isDefined
wenzelm@36685
    66
    def next(): CharSequence =
wenzelm@36685
    67
      state match {
wenzelm@36685
    68
        case Some((s, i)) => { state = next_chunk(i); s }
wenzelm@36685
    69
        case None => throw new NoSuchElementException("next on empty iterator")
wenzelm@36685
    70
      }
wenzelm@36685
    71
  }
wenzelm@36685
    72
wenzelm@36685
    73
wenzelm@34216
    74
  /* simple dialogs */
wenzelm@34216
    75
wenzelm@34216
    76
  private def simple_dialog(kind: Int, default_title: String)
wenzelm@34216
    77
    (parent: Component, title: String, message: Any*)
wenzelm@34216
    78
  {
wenzelm@36791
    79
    Swing_Thread.now {
wenzelm@36791
    80
      JOptionPane.showMessageDialog(parent,
wenzelm@36791
    81
        message.toArray.asInstanceOf[Array[AnyRef]],
wenzelm@36791
    82
        if (title == null) default_title else title, kind)
wenzelm@36791
    83
    }
wenzelm@34216
    84
  }
wenzelm@34216
    85
wenzelm@34216
    86
  def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _
wenzelm@34216
    87
  def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
wenzelm@34216
    88
  def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
wenzelm@34216
    89
wenzelm@34216
    90
wenzelm@34136
    91
  /* timing */
wenzelm@34136
    92
wenzelm@34314
    93
  def timeit[A](message: String)(e: => A) =
wenzelm@34136
    94
  {
wenzelm@34136
    95
    val start = System.currentTimeMillis()
wenzelm@34136
    96
    val result = Exn.capture(e)
wenzelm@34136
    97
    val stop = System.currentTimeMillis()
wenzelm@34314
    98
    System.err.println(
wenzelm@34317
    99
      (if (message.isEmpty) "" else message + ": ") + (stop - start) + "ms elapsed time")
wenzelm@34136
   100
    Exn.release(result)
wenzelm@34136
   101
  }
wenzelm@34136
   102
}