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