src/Pure/library.scala
author wenzelm
Fri May 28 20:41:23 2010 +0200 (2010-05-28)
changeset 37174 6feaab4fc27d
parent 37048 d014976dd690
child 37686 bb27d99a9a69
permissions -rw-r--r--
assume given SCALA_HOME, e.g. from component settings or external setup;
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@37018
    14
import scala.swing.ComboBox
wenzelm@37018
    15
import scala.swing.event.SelectionChanged
wenzelm@37018
    16
wenzelm@37018
    17
wenzelm@34136
    18
object Library
wenzelm@34136
    19
{
wenzelm@37035
    20
  /* partial functions */
wenzelm@37035
    21
wenzelm@37035
    22
  def undefined[A, B] = new PartialFunction[A, B] {
wenzelm@37035
    23
    def apply(x: A): B = throw new NoSuchElementException("undefined")
wenzelm@37035
    24
    def isDefinedAt(x: A) = false
wenzelm@37035
    25
  }
wenzelm@37035
    26
wenzelm@37035
    27
wenzelm@36688
    28
  /* separate */
wenzelm@36688
    29
wenzelm@36688
    30
  def separate[A](s: A, list: List[A]): List[A] =
wenzelm@36688
    31
    list match {
wenzelm@36688
    32
      case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs)
wenzelm@36688
    33
      case _ => list
wenzelm@36688
    34
    }
wenzelm@36688
    35
wenzelm@36688
    36
wenzelm@34141
    37
  /* reverse CharSequence */
wenzelm@34141
    38
wenzelm@34141
    39
  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
wenzelm@34141
    40
  {
wenzelm@34141
    41
    require(0 <= start && start <= end && end <= text.length)
wenzelm@34141
    42
wenzelm@34141
    43
    def this(text: CharSequence) = this(text, 0, text.length)
wenzelm@34141
    44
wenzelm@34141
    45
    def length: Int = end - start
wenzelm@34141
    46
    def charAt(i: Int): Char = text.charAt(end - i - 1)
wenzelm@34141
    47
wenzelm@34141
    48
    def subSequence(i: Int, j: Int): CharSequence =
wenzelm@34141
    49
      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
wenzelm@34141
    50
      else throw new IndexOutOfBoundsException
wenzelm@34141
    51
wenzelm@34141
    52
    override def toString: String =
wenzelm@34141
    53
    {
wenzelm@34141
    54
      val buf = new StringBuilder(length)
wenzelm@34141
    55
      for (i <- 0 until length)
wenzelm@34141
    56
        buf.append(charAt(i))
wenzelm@34141
    57
      buf.toString
wenzelm@34141
    58
    }
wenzelm@34141
    59
  }
wenzelm@34141
    60
wenzelm@34141
    61
wenzelm@36685
    62
  /* iterate over chunks (cf. space_explode/split_lines in ML) */
wenzelm@36685
    63
wenzelm@36685
    64
  def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
wenzelm@36685
    65
  {
wenzelm@36685
    66
    private val end = source.length
wenzelm@36685
    67
    private def next_chunk(i: Int): Option[(CharSequence, Int)] =
wenzelm@36685
    68
    {
wenzelm@36685
    69
      if (i < end) {
wenzelm@36685
    70
        var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
wenzelm@36685
    71
        Some((source.subSequence(i + 1, j), j))
wenzelm@36685
    72
      }
wenzelm@36685
    73
      else None
wenzelm@36685
    74
    }
wenzelm@36685
    75
    private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
wenzelm@36685
    76
wenzelm@36685
    77
    def hasNext(): Boolean = state.isDefined
wenzelm@36685
    78
    def next(): CharSequence =
wenzelm@36685
    79
      state match {
wenzelm@36685
    80
        case Some((s, i)) => { state = next_chunk(i); s }
wenzelm@36685
    81
        case None => throw new NoSuchElementException("next on empty iterator")
wenzelm@36685
    82
      }
wenzelm@36685
    83
  }
wenzelm@36685
    84
wenzelm@36685
    85
wenzelm@34216
    86
  /* simple dialogs */
wenzelm@34216
    87
wenzelm@34216
    88
  private def simple_dialog(kind: Int, default_title: String)
wenzelm@34216
    89
    (parent: Component, title: String, message: Any*)
wenzelm@34216
    90
  {
wenzelm@36791
    91
    Swing_Thread.now {
wenzelm@36791
    92
      JOptionPane.showMessageDialog(parent,
wenzelm@36791
    93
        message.toArray.asInstanceOf[Array[AnyRef]],
wenzelm@36791
    94
        if (title == null) default_title else title, kind)
wenzelm@36791
    95
    }
wenzelm@34216
    96
  }
wenzelm@34216
    97
wenzelm@34216
    98
  def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _
wenzelm@34216
    99
  def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
wenzelm@34216
   100
  def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
wenzelm@34216
   101
wenzelm@34216
   102
wenzelm@37018
   103
  /* zoom box */
wenzelm@37018
   104
wenzelm@37048
   105
  class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
wenzelm@37048
   106
    List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
wenzelm@37048
   107
  {
wenzelm@37048
   108
    val Factor = "([0-9]+)%?"r
wenzelm@37048
   109
    def parse(text: String): Int =
wenzelm@37048
   110
      text match {
wenzelm@37048
   111
        case Factor(s) =>
wenzelm@37048
   112
          val i = Integer.parseInt(s)
wenzelm@37048
   113
          if (10 <= i && i <= 1000) i else 100
wenzelm@37048
   114
        case _ => 100
wenzelm@37048
   115
      }
wenzelm@37048
   116
    def print(i: Int): String = i.toString + "%"
wenzelm@37018
   117
wenzelm@37048
   118
    makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
wenzelm@37048
   119
    reactions += {
wenzelm@37048
   120
      case SelectionChanged(_) => apply_factor(parse(selection.item))
wenzelm@37018
   121
    }
wenzelm@37048
   122
    listenTo(selection)
wenzelm@37048
   123
    selection.index = 3
wenzelm@37048
   124
    prototypeDisplayValue = Some("00000%")
wenzelm@37048
   125
  }
wenzelm@37018
   126
wenzelm@37018
   127
wenzelm@34136
   128
  /* timing */
wenzelm@34136
   129
wenzelm@34314
   130
  def timeit[A](message: String)(e: => A) =
wenzelm@34136
   131
  {
wenzelm@34136
   132
    val start = System.currentTimeMillis()
wenzelm@34136
   133
    val result = Exn.capture(e)
wenzelm@34136
   134
    val stop = System.currentTimeMillis()
wenzelm@34314
   135
    System.err.println(
wenzelm@34317
   136
      (if (message.isEmpty) "" else message + ": ") + (stop - start) + "ms elapsed time")
wenzelm@34136
   137
    Exn.release(result)
wenzelm@34136
   138
  }
wenzelm@34136
   139
}