src/Pure/library.scala
author wenzelm
Fri Apr 12 14:54:14 2013 +0200 (2013-04-12)
changeset 51700 c8f2bad67dbb
parent 51616 949e2cf02a3d
child 51981 a8ffd3692f57
permissions -rw-r--r--
tuned signature;
tuned comments;
     1 /*  Title:      Pure/library.scala
     2     Module:     PIDE
     3     Author:     Makarius
     4 
     5 Basic library.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import java.util.Locale
    12 import java.util.concurrent.{Future => JFuture, TimeUnit}
    13 
    14 
    15 object Library
    16 {
    17   /* user errors */
    18 
    19   object ERROR
    20   {
    21     def apply(message: String): Throwable = new RuntimeException(message)
    22     def unapply(exn: Throwable): Option[String] = Exn.user_message(exn)
    23   }
    24 
    25   def error(message: String): Nothing = throw ERROR(message)
    26 
    27   def cat_error(msg1: String, msg2: String): Nothing =
    28     if (msg1 == "") error(msg1)
    29     else error(msg1 + "\n" + msg2)
    30 
    31 
    32   /* separated chunks */
    33 
    34   def separate[A](s: A, list: List[A]): List[A] =
    35     list match {
    36       case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs)
    37       case _ => list
    38     }
    39 
    40   def separated_chunks(sep: Char, source: CharSequence): Iterator[CharSequence] =
    41     new Iterator[CharSequence] {
    42       private val end = source.length
    43       private def next_chunk(i: Int): Option[(CharSequence, Int)] =
    44       {
    45         if (i < end) {
    46           var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
    47           Some((source.subSequence(i + 1, j), j))
    48         }
    49         else None
    50       }
    51       private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
    52 
    53       def hasNext(): Boolean = state.isDefined
    54       def next(): CharSequence =
    55         state match {
    56           case Some((s, i)) => { state = next_chunk(i); s }
    57           case None => Iterator.empty.next()
    58         }
    59     }
    60 
    61   def space_explode(sep: Char, str: String): List[String] =
    62     separated_chunks(sep, str).map(_.toString).toList
    63 
    64 
    65   /* lines */
    66 
    67   def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
    68 
    69   def split_lines(str: String): List[String] = space_explode('\n', str)
    70 
    71   def first_line(source: CharSequence): String =
    72   {
    73     val lines = separated_chunks('\n', source)
    74     if (lines.hasNext) lines.next.toString
    75     else ""
    76   }
    77 
    78 
    79   /* strings */
    80 
    81   def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH)
    82   def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH)
    83 
    84   def capitalize(str: String): String =
    85     if (str.length == 0) str
    86     else uppercase(str.substring(0, 1)) + str.substring(1)
    87 
    88   def try_unprefix(prfx: String, s: String): Option[String] =
    89     if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
    90 
    91 
    92   /* quote */
    93 
    94   def quote(s: String): String = "\"" + s + "\""
    95   def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
    96   def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
    97 
    98 
    99   /* reverse CharSequence */
   100 
   101   class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
   102   {
   103     require(0 <= start && start <= end && end <= text.length)
   104 
   105     def this(text: CharSequence) = this(text, 0, text.length)
   106 
   107     def length: Int = end - start
   108     def charAt(i: Int): Char = text.charAt(end - i - 1)
   109 
   110     def subSequence(i: Int, j: Int): CharSequence =
   111       if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
   112       else throw new IndexOutOfBoundsException
   113 
   114     override def toString: String =
   115     {
   116       val buf = new StringBuilder(length)
   117       for (i <- 0 until length)
   118         buf.append(charAt(i))
   119       buf.toString
   120     }
   121   }
   122 
   123 
   124   /* Java futures */
   125 
   126   def future_value[A](x: A) = new JFuture[A]
   127   {
   128     def cancel(may_interrupt: Boolean): Boolean = false
   129     def isCancelled(): Boolean = false
   130     def isDone(): Boolean = true
   131     def get(): A = x
   132     def get(timeout: Long, time_unit: TimeUnit): A = x
   133   }
   134 }
   135 
   136 
   137 class Basic_Library
   138 {
   139   val ERROR = Library.ERROR
   140   val error = Library.error _
   141   val cat_error = Library.cat_error _
   142 
   143   val space_explode = Library.space_explode _
   144   val split_lines = Library.split_lines _
   145   val cat_lines = Library.cat_lines _
   146   val quote = Library.quote _
   147   val commas = Library.commas _
   148   val commas_quote = Library.commas_quote _
   149 
   150 
   151   /* parallel tasks */
   152 
   153   implicit def function_as_callable[A](f: () => A) =
   154     new java.util.concurrent.Callable[A] { def call = f() }
   155 
   156   val default_thread_pool =
   157     scala.collection.parallel.ThreadPoolTasks.defaultThreadPool
   158 }