src/Pure/library.scala
author wenzelm
Fri Apr 25 20:07:39 2014 +0200 (2014-04-25)
changeset 56728 6dc97c5aaf5e
parent 56688 f3932166a33d
child 56730 e723f041b6d0
permissions -rw-r--r--
unused;
     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.concurrent.{Future => JFuture, TimeUnit}
    14 
    15 
    16 object Library
    17 {
    18   /* user errors */
    19 
    20   object ERROR
    21   {
    22     def apply(message: String): Throwable = new RuntimeException(message)
    23     def unapply(exn: Throwable): Option[String] = Exn.user_message(exn)
    24   }
    25 
    26   def error(message: String): Nothing = throw ERROR(message)
    27 
    28   def cat_message(msg1: String, msg2: String): String =
    29     if (msg1 == "") msg2
    30     else msg1 + "\n" + msg2
    31 
    32   def cat_error(msg1: String, msg2: String): Nothing =
    33     error(cat_message(msg1, msg2))
    34 
    35 
    36   /* separated chunks */
    37 
    38   def separate[A](s: A, list: List[A]): List[A] =
    39   {
    40     val result = new mutable.ListBuffer[A]
    41     var first = true
    42     for (x <- list) {
    43       if (first) {
    44         first = false
    45         result += x
    46       }
    47       else {
    48         result += s
    49         result += x
    50       }
    51     }
    52     result.toList
    53   }
    54 
    55   def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] =
    56     new Iterator[CharSequence] {
    57       private val end = source.length
    58       private def next_chunk(i: Int): Option[(CharSequence, Int)] =
    59       {
    60         if (i < end) {
    61           var j = i; do j += 1 while (j < end && !sep(source.charAt(j)))
    62           Some((source.subSequence(i + 1, j), j))
    63         }
    64         else None
    65       }
    66       private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
    67 
    68       def hasNext(): Boolean = state.isDefined
    69       def next(): CharSequence =
    70         state match {
    71           case Some((s, i)) => { state = next_chunk(i); s }
    72           case None => Iterator.empty.next()
    73         }
    74     }
    75 
    76   def space_explode(sep: Char, str: String): List[String] =
    77     separated_chunks(_ == sep, str).map(_.toString).toList
    78 
    79 
    80   /* lines */
    81 
    82   def terminate_lines(lines: Iterable[CharSequence]): Iterable[CharSequence] =
    83     new Iterable[CharSequence] {
    84       def iterator: Iterator[CharSequence] =
    85         lines.iterator.map(line => new Line_Termination(line))
    86     }
    87 
    88   def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
    89 
    90   def split_lines(str: String): List[String] = space_explode('\n', str)
    91 
    92   def first_line(source: CharSequence): String =
    93   {
    94     val lines = separated_chunks(_ == '\n', source)
    95     if (lines.hasNext) lines.next.toString
    96     else ""
    97   }
    98 
    99 
   100   /* strings */
   101 
   102   def try_unprefix(prfx: String, s: String): Option[String] =
   103     if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
   104 
   105   def try_unsuffix(sffx: String, s: String): Option[String] =
   106     if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None
   107 
   108   def trim_line(s: String): String =
   109     if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
   110     else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
   111     else s
   112 
   113 
   114   /* quote */
   115 
   116   def quote(s: String): String = "\"" + s + "\""
   117   def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
   118   def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
   119 
   120 
   121   /* CharSequence */
   122 
   123   class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
   124   {
   125     require(0 <= start && start <= end && end <= text.length)
   126 
   127     def this(text: CharSequence) = this(text, 0, text.length)
   128 
   129     def length: Int = end - start
   130     def charAt(i: Int): Char = text.charAt(end - i - 1)
   131 
   132     def subSequence(i: Int, j: Int): CharSequence =
   133       if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
   134       else throw new IndexOutOfBoundsException
   135 
   136     override def toString: String =
   137     {
   138       val buf = new StringBuilder(length)
   139       for (i <- 0 until length)
   140         buf.append(charAt(i))
   141       buf.toString
   142     }
   143   }
   144 
   145   class Line_Termination(text: CharSequence) extends CharSequence
   146   {
   147     def length: Int = text.length + 1
   148     def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i)
   149     def subSequence(i: Int, j: Int): CharSequence =
   150       if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1))
   151       else text.subSequence(i, j)
   152     override def toString: String = text.toString + "\n"
   153   }
   154 
   155 
   156   /* canonical list operations */
   157 
   158   def member[A, B](xs: List[A])(x: B): Boolean = xs.exists(_ == x)
   159   def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   160   def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   161   def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
   162 }
   163 
   164 
   165 class Basic_Library
   166 {
   167   val ERROR = Library.ERROR
   168   val error = Library.error _
   169   val cat_error = Library.cat_error _
   170 
   171   val space_explode = Library.space_explode _
   172   val split_lines = Library.split_lines _
   173   val cat_lines = Library.cat_lines _
   174   val quote = Library.quote _
   175   val commas = Library.commas _
   176   val commas_quote = Library.commas_quote _
   177 
   178 
   179   /* parallel tasks */
   180 
   181   implicit def function_as_callable[A](f: () => A) =
   182     new java.util.concurrent.Callable[A] { def call = f() }
   183 
   184   val default_thread_pool =
   185     scala.collection.parallel.ForkJoinTasks.defaultForkJoinPool
   186 }