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