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