src/Pure/library.scala
author wenzelm
Mon Mar 10 15:04:01 2014 +0100 (2014-03-10)
changeset 56026 893fe12639bc
parent 55977 ec4830499634
child 56552 76cf86240cb7
permissions -rw-r--r--
tuned signature -- prefer Name_Space.get with its builtin error;
     1 /*  Title:      Pure/library.scala
     2     Module:     PIDE
     3     Author:     Makarius
     4 
     5 Basic library.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 import scala.collection.mutable
    12 
    13 import java.util.Locale
    14 import java.util.concurrent.{Future => JFuture, TimeUnit}
    15 
    16 
    17 object Library
    18 {
    19   /* user errors */
    20 
    21   object ERROR
    22   {
    23     def apply(message: String): Throwable = new RuntimeException(message)
    24     def unapply(exn: Throwable): Option[String] = Exn.user_message(exn)
    25   }
    26 
    27   def error(message: String): Nothing = throw ERROR(message)
    28 
    29   def cat_message(msg1: String, msg2: String): String =
    30     if (msg1 == "") msg2
    31     else msg1 + "\n" + msg2
    32 
    33   def cat_error(msg1: String, msg2: String): Nothing =
    34     error(cat_message(msg1, msg2))
    35 
    36 
    37   /* separated chunks */
    38 
    39   def separate[A](s: A, list: List[A]): List[A] =
    40   {
    41     val result = new mutable.ListBuffer[A]
    42     var first = true
    43     for (x <- list) {
    44       if (first) {
    45         first = false
    46         result += x
    47       }
    48       else {
    49         result += s
    50         result += x
    51       }
    52     }
    53     result.toList
    54   }
    55 
    56   def separated_chunks(sep: Char, source: CharSequence): Iterator[CharSequence] =
    57     new Iterator[CharSequence] {
    58       private val end = source.length
    59       private def next_chunk(i: Int): Option[(CharSequence, Int)] =
    60       {
    61         if (i < end) {
    62           var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
    63           Some((source.subSequence(i + 1, j), j))
    64         }
    65         else None
    66       }
    67       private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
    68 
    69       def hasNext(): Boolean = state.isDefined
    70       def next(): CharSequence =
    71         state match {
    72           case Some((s, i)) => { state = next_chunk(i); s }
    73           case None => Iterator.empty.next()
    74         }
    75     }
    76 
    77   def space_explode(sep: Char, str: String): List[String] =
    78     separated_chunks(sep, str).map(_.toString).toList
    79 
    80 
    81   /* lines */
    82 
    83   def terminate_lines(lines: Iterable[CharSequence]): Iterable[CharSequence] =
    84     new Iterable[CharSequence] {
    85       def iterator: Iterator[CharSequence] =
    86         lines.iterator.map(line => new Line_Termination(line))
    87     }
    88 
    89   def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
    90 
    91   def split_lines(str: String): List[String] = space_explode('\n', str)
    92 
    93   def first_line(source: CharSequence): String =
    94   {
    95     val lines = separated_chunks('\n', source)
    96     if (lines.hasNext) lines.next.toString
    97     else ""
    98   }
    99 
   100   def plain_words(str: String): String =
   101     space_explode('_', str).mkString(" ")
   102 
   103 
   104   /* strings */
   105 
   106   def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH)
   107   def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH)
   108 
   109   def capitalize(str: String): String =
   110     if (str.length == 0) str
   111     else uppercase(str.substring(0, 1)) + str.substring(1)
   112 
   113   def try_unprefix(prfx: String, s: String): Option[String] =
   114     if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
   115 
   116   def try_unsuffix(sffx: String, s: String): Option[String] =
   117     if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None
   118 
   119   def trim_line(s: String): String =
   120     if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
   121     else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
   122     else s
   123 
   124 
   125   /* quote */
   126 
   127   def quote(s: String): String = "\"" + s + "\""
   128   def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
   129   def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
   130 
   131 
   132   /* CharSequence */
   133 
   134   class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
   135   {
   136     require(0 <= start && start <= end && end <= text.length)
   137 
   138     def this(text: CharSequence) = this(text, 0, text.length)
   139 
   140     def length: Int = end - start
   141     def charAt(i: Int): Char = text.charAt(end - i - 1)
   142 
   143     def subSequence(i: Int, j: Int): CharSequence =
   144       if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
   145       else throw new IndexOutOfBoundsException
   146 
   147     override def toString: String =
   148     {
   149       val buf = new StringBuilder(length)
   150       for (i <- 0 until length)
   151         buf.append(charAt(i))
   152       buf.toString
   153     }
   154   }
   155 
   156   class Line_Termination(text: CharSequence) extends CharSequence
   157   {
   158     def length: Int = text.length + 1
   159     def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i)
   160     def subSequence(i: Int, j: Int): CharSequence =
   161       if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1))
   162       else text.subSequence(i, j)
   163     override def toString: String = text.toString + "\n"
   164   }
   165 
   166 
   167   /* Java futures */
   168 
   169   def future_value[A](x: A) = new JFuture[A]
   170   {
   171     def cancel(may_interrupt: Boolean): Boolean = false
   172     def isCancelled(): Boolean = false
   173     def isDone(): Boolean = true
   174     def get(): A = x
   175     def get(timeout: Long, time_unit: TimeUnit): A = x
   176   }
   177 }
   178 
   179 
   180 class Basic_Library
   181 {
   182   val ERROR = Library.ERROR
   183   val error = Library.error _
   184   val cat_error = Library.cat_error _
   185 
   186   val space_explode = Library.space_explode _
   187   val split_lines = Library.split_lines _
   188   val cat_lines = Library.cat_lines _
   189   val quote = Library.quote _
   190   val commas = Library.commas _
   191   val commas_quote = Library.commas_quote _
   192 
   193 
   194   /* parallel tasks */
   195 
   196   implicit def function_as_callable[A](f: () => A) =
   197     new java.util.concurrent.Callable[A] { def call = f() }
   198 
   199   val default_thread_pool =
   200     scala.collection.parallel.ThreadPoolTasks.defaultThreadPool
   201 }