src/Pure/library.scala
author wenzelm
Mon, 28 Dec 2009 18:40:13 +0100
changeset 34198 ff5486262cd6
parent 34196 c352f679dcca
child 34216 ada8eb23a08e
permissions -rw-r--r--
moved Library.decode_permissive_utf8 to Isabelle_System;
moved Library.with_tmp_file to Isabelle_System;
added Isabelle_System.read_file/write_file;
added Isabelle_System.system_out, with propagation of thread interrupts and process shutdown (global CTRL-C);
     1 /*  Title:      Pure/library.scala
     2     Author:     Makarius
     3 
     4 Basic library.
     5 */
     6 
     7 package isabelle
     8 
     9 import java.lang.System
    10 
    11 
    12 object Library
    13 {
    14   /* reverse CharSequence */
    15 
    16   class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
    17   {
    18     require(0 <= start && start <= end && end <= text.length)
    19 
    20     def this(text: CharSequence) = this(text, 0, text.length)
    21 
    22     def length: Int = end - start
    23     def charAt(i: Int): Char = text.charAt(end - i - 1)
    24 
    25     def subSequence(i: Int, j: Int): CharSequence =
    26       if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
    27       else throw new IndexOutOfBoundsException
    28 
    29     override def toString: String =
    30     {
    31       val buf = new StringBuilder(length)
    32       for (i <- 0 until length)
    33         buf.append(charAt(i))
    34       buf.toString
    35     }
    36   }
    37 
    38 
    39   /* timing */
    40 
    41   def timeit[A](e: => A) =
    42   {
    43     val start = System.currentTimeMillis()
    44     val result = Exn.capture(e)
    45     val stop = System.currentTimeMillis()
    46     System.err.println((stop - start) + "ms elapsed time")
    47     Exn.release(result)
    48   }
    49 }