src/Pure/library.scala
author wenzelm
Thu, 06 May 2010 21:02:34 +0200
changeset 36685 2b3076cfd6dd
parent 34317 c1509b9d624f
child 36688 321d392ab12e
permissions -rw-r--r--
slightly more general Library.chunks;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/library.scala
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     3
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     4
Basic library.
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     5
*/
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     6
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     7
package isabelle
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     8
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
     9
import java.lang.System
34216
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    10
import java.awt.Component
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    11
import javax.swing.JOptionPane
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    12
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    13
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    14
object Library
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    15
{
34141
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    16
  /* reverse CharSequence */
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    17
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    18
  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    19
  {
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    20
    require(0 <= start && start <= end && end <= text.length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    21
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    22
    def this(text: CharSequence) = this(text, 0, text.length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    23
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    24
    def length: Int = end - start
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    25
    def charAt(i: Int): Char = text.charAt(end - i - 1)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    26
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    27
    def subSequence(i: Int, j: Int): CharSequence =
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    28
      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    29
      else throw new IndexOutOfBoundsException
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    30
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    31
    override def toString: String =
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    32
    {
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    33
      val buf = new StringBuilder(length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    34
      for (i <- 0 until length)
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    35
        buf.append(charAt(i))
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    36
      buf.toString
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    37
    }
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    38
  }
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    39
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34136
diff changeset
    40
36685
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    41
  /* iterate over chunks (cf. space_explode/split_lines in ML) */
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    42
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    43
  def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    44
  {
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    45
    private val end = source.length
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    46
    private def next_chunk(i: Int): Option[(CharSequence, Int)] =
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    47
    {
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    48
      if (i < end) {
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    49
        var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    50
        Some((source.subSequence(i + 1, j), j))
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    51
      }
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    52
      else None
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    53
    }
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    54
    private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    55
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    56
    def hasNext(): Boolean = state.isDefined
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    57
    def next(): CharSequence =
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    58
      state match {
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    59
        case Some((s, i)) => { state = next_chunk(i); s }
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    60
        case None => throw new NoSuchElementException("next on empty iterator")
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    61
      }
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    62
  }
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    63
2b3076cfd6dd slightly more general Library.chunks;
wenzelm
parents: 34317
diff changeset
    64
34216
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    65
  /* simple dialogs */
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    66
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    67
  private def simple_dialog(kind: Int, default_title: String)
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    68
    (parent: Component, title: String, message: Any*)
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    69
  {
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    70
    JOptionPane.showMessageDialog(parent,
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    71
      message.toArray.asInstanceOf[Array[AnyRef]],
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    72
      if (title == null) default_title else title, kind)
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    73
  }
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    74
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    75
  def dialog = simple_dialog(JOptionPane.PLAIN_MESSAGE, null) _
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    76
  def warning_dialog = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning") _
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    77
  def error_dialog = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error") _
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    78
ada8eb23a08e added simple dialogs;
wenzelm
parents: 34198
diff changeset
    79
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    80
  /* timing */
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    81
34314
f799f3749596 timeit message;
wenzelm
parents: 34216
diff changeset
    82
  def timeit[A](message: String)(e: => A) =
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    83
  {
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    84
    val start = System.currentTimeMillis()
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    85
    val result = Exn.capture(e)
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    86
    val stop = System.currentTimeMillis()
34314
f799f3749596 timeit message;
wenzelm
parents: 34216
diff changeset
    87
    System.err.println(
34317
c1509b9d624f tuned message;
wenzelm
parents: 34314
diff changeset
    88
      (if (message.isEmpty) "" else message + ": ") + (stop - start) + "ms elapsed time")
34136
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    89
    Exn.release(result)
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    90
  }
3dcb46ae6185 added basic library -- Scala version;
wenzelm
parents:
diff changeset
    91
}