src/Pure/library.scala
author wenzelm
Sun Dec 20 15:44:07 2009 +0100 (2009-12-20 ago)
changeset 34141 297b2149077d
parent 34136 3dcb46ae6185
child 34191 b6960fc09ef3
permissions -rw-r--r--
simiplified result of keyword parser (again);
sort completions by plain string order;
moved Reverse to library.scala;
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@34136
    10
wenzelm@34136
    11
wenzelm@34136
    12
object Library
wenzelm@34136
    13
{
wenzelm@34141
    14
  /* reverse CharSequence */
wenzelm@34141
    15
wenzelm@34141
    16
  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
wenzelm@34141
    17
  {
wenzelm@34141
    18
    require(0 <= start && start <= end && end <= text.length)
wenzelm@34141
    19
wenzelm@34141
    20
    def this(text: CharSequence) = this(text, 0, text.length)
wenzelm@34141
    21
wenzelm@34141
    22
    def length: Int = end - start
wenzelm@34141
    23
    def charAt(i: Int): Char = text.charAt(end - i - 1)
wenzelm@34141
    24
wenzelm@34141
    25
    def subSequence(i: Int, j: Int): CharSequence =
wenzelm@34141
    26
      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
wenzelm@34141
    27
      else throw new IndexOutOfBoundsException
wenzelm@34141
    28
wenzelm@34141
    29
    override def toString: String =
wenzelm@34141
    30
    {
wenzelm@34141
    31
      val buf = new StringBuilder(length)
wenzelm@34141
    32
      for (i <- 0 until length)
wenzelm@34141
    33
        buf.append(charAt(i))
wenzelm@34141
    34
      buf.toString
wenzelm@34141
    35
    }
wenzelm@34141
    36
  }
wenzelm@34141
    37
wenzelm@34141
    38
wenzelm@34136
    39
  /* timing */
wenzelm@34136
    40
wenzelm@34136
    41
  def timeit[A](e: => A) =
wenzelm@34136
    42
  {
wenzelm@34136
    43
    val start = System.currentTimeMillis()
wenzelm@34136
    44
    val result = Exn.capture(e)
wenzelm@34136
    45
    val stop = System.currentTimeMillis()
wenzelm@34136
    46
    System.err.println((stop - start) + "ms elapsed time")
wenzelm@34136
    47
    Exn.release(result)
wenzelm@34136
    48
  }
wenzelm@34136
    49
}