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