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