src/Pure/library.scala
author wenzelm
Fri Apr 12 14:54:14 2013 +0200 (2013-04-12)
changeset 51700 c8f2bad67dbb
parent 51616 949e2cf02a3d
child 51981 a8ffd3692f57
permissions -rw-r--r--
tuned signature;
tuned comments;
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@49245
    11
import java.util.Locale
wenzelm@50414
    12
import java.util.concurrent.{Future => JFuture, TimeUnit}
wenzelm@37018
    13
wenzelm@37018
    14
wenzelm@34136
    15
object Library
wenzelm@34136
    16
{
wenzelm@43652
    17
  /* user errors */
wenzelm@43652
    18
wenzelm@43652
    19
  object ERROR
wenzelm@43652
    20
  {
wenzelm@43652
    21
    def apply(message: String): Throwable = new RuntimeException(message)
wenzelm@48479
    22
    def unapply(exn: Throwable): Option[String] = Exn.user_message(exn)
wenzelm@43652
    23
  }
wenzelm@43652
    24
wenzelm@43652
    25
  def error(message: String): Nothing = throw ERROR(message)
wenzelm@43652
    26
wenzelm@43652
    27
  def cat_error(msg1: String, msg2: String): Nothing =
wenzelm@43652
    28
    if (msg1 == "") error(msg1)
wenzelm@43652
    29
    else error(msg1 + "\n" + msg2)
wenzelm@43652
    30
wenzelm@43652
    31
wenzelm@48996
    32
  /* separated chunks */
wenzelm@36688
    33
wenzelm@36688
    34
  def separate[A](s: A, list: List[A]): List[A] =
wenzelm@36688
    35
    list match {
wenzelm@36688
    36
      case x :: xs if !xs.isEmpty => x :: s :: separate(s, xs)
wenzelm@36688
    37
      case _ => list
wenzelm@36688
    38
    }
wenzelm@36688
    39
wenzelm@48996
    40
  def separated_chunks(sep: Char, source: CharSequence): Iterator[CharSequence] =
wenzelm@48996
    41
    new Iterator[CharSequence] {
wenzelm@48996
    42
      private val end = source.length
wenzelm@48996
    43
      private def next_chunk(i: Int): Option[(CharSequence, Int)] =
wenzelm@48996
    44
      {
wenzelm@48996
    45
        if (i < end) {
wenzelm@48996
    46
          var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
wenzelm@48996
    47
          Some((source.subSequence(i + 1, j), j))
wenzelm@48996
    48
        }
wenzelm@48996
    49
        else None
wenzelm@43598
    50
      }
wenzelm@48996
    51
      private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
wenzelm@48996
    52
wenzelm@48996
    53
      def hasNext(): Boolean = state.isDefined
wenzelm@48996
    54
      def next(): CharSequence =
wenzelm@48996
    55
        state match {
wenzelm@48996
    56
          case Some((s, i)) => { state = next_chunk(i); s }
wenzelm@48996
    57
          case None => Iterator.empty.next()
wenzelm@48996
    58
        }
wenzelm@43598
    59
    }
wenzelm@43598
    60
wenzelm@48996
    61
  def space_explode(sep: Char, str: String): List[String] =
wenzelm@48996
    62
    separated_chunks(sep, str).map(_.toString).toList
wenzelm@48996
    63
wenzelm@48996
    64
wenzelm@48996
    65
  /* lines */
wenzelm@48996
    66
wenzelm@48996
    67
  def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
wenzelm@48996
    68
wenzelm@43670
    69
  def split_lines(str: String): List[String] = space_explode('\n', str)
wenzelm@43670
    70
wenzelm@48996
    71
  def first_line(source: CharSequence): String =
wenzelm@48996
    72
  {
wenzelm@48996
    73
    val lines = separated_chunks('\n', source)
wenzelm@48996
    74
    if (lines.hasNext) lines.next.toString
wenzelm@48996
    75
    else ""
wenzelm@48996
    76
  }
wenzelm@48996
    77
wenzelm@50847
    78
wenzelm@50847
    79
  /* strings */
wenzelm@50847
    80
wenzelm@50299
    81
  def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH)
wenzelm@50299
    82
  def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH)
wenzelm@50299
    83
wenzelm@49245
    84
  def capitalize(str: String): String =
wenzelm@49245
    85
    if (str.length == 0) str
wenzelm@50299
    86
    else uppercase(str.substring(0, 1)) + str.substring(1)
wenzelm@49245
    87
wenzelm@50847
    88
  def try_unprefix(prfx: String, s: String): Option[String] =
wenzelm@50847
    89
    if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
wenzelm@50847
    90
wenzelm@43598
    91
wenzelm@48996
    92
  /* quote */
wenzelm@46196
    93
wenzelm@43598
    94
  def quote(s: String): String = "\"" + s + "\""
wenzelm@43598
    95
  def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
wenzelm@48362
    96
  def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
wenzelm@43598
    97
wenzelm@36688
    98
wenzelm@34141
    99
  /* reverse CharSequence */
wenzelm@34141
   100
wenzelm@34141
   101
  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
wenzelm@34141
   102
  {
wenzelm@34141
   103
    require(0 <= start && start <= end && end <= text.length)
wenzelm@34141
   104
wenzelm@34141
   105
    def this(text: CharSequence) = this(text, 0, text.length)
wenzelm@34141
   106
wenzelm@34141
   107
    def length: Int = end - start
wenzelm@34141
   108
    def charAt(i: Int): Char = text.charAt(end - i - 1)
wenzelm@34141
   109
wenzelm@34141
   110
    def subSequence(i: Int, j: Int): CharSequence =
wenzelm@34141
   111
      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
wenzelm@34141
   112
      else throw new IndexOutOfBoundsException
wenzelm@34141
   113
wenzelm@34141
   114
    override def toString: String =
wenzelm@34141
   115
    {
wenzelm@34141
   116
      val buf = new StringBuilder(length)
wenzelm@34141
   117
      for (i <- 0 until length)
wenzelm@34141
   118
        buf.append(charAt(i))
wenzelm@34141
   119
      buf.toString
wenzelm@34141
   120
    }
wenzelm@34141
   121
  }
wenzelm@34141
   122
wenzelm@34141
   123
wenzelm@50414
   124
  /* Java futures */
wenzelm@50414
   125
wenzelm@50414
   126
  def future_value[A](x: A) = new JFuture[A]
wenzelm@50414
   127
  {
wenzelm@50414
   128
    def cancel(may_interrupt: Boolean): Boolean = false
wenzelm@50414
   129
    def isCancelled(): Boolean = false
wenzelm@50414
   130
    def isDone(): Boolean = true
wenzelm@50414
   131
    def get(): A = x
wenzelm@50414
   132
    def get(timeout: Long, time_unit: TimeUnit): A = x
wenzelm@50414
   133
  }
wenzelm@34136
   134
}
wenzelm@43652
   135
wenzelm@43652
   136
wenzelm@43652
   137
class Basic_Library
wenzelm@43652
   138
{
wenzelm@43670
   139
  val ERROR = Library.ERROR
wenzelm@43670
   140
  val error = Library.error _
wenzelm@43670
   141
  val cat_error = Library.cat_error _
wenzelm@43670
   142
wenzelm@43652
   143
  val space_explode = Library.space_explode _
wenzelm@43670
   144
  val split_lines = Library.split_lines _
wenzelm@46196
   145
  val cat_lines = Library.cat_lines _
wenzelm@43652
   146
  val quote = Library.quote _
wenzelm@43652
   147
  val commas = Library.commas _
wenzelm@43652
   148
  val commas_quote = Library.commas_quote _
wenzelm@49470
   149
wenzelm@49470
   150
wenzelm@49470
   151
  /* parallel tasks */
wenzelm@49470
   152
wenzelm@49470
   153
  implicit def function_as_callable[A](f: () => A) =
wenzelm@49470
   154
    new java.util.concurrent.Callable[A] { def call = f() }
wenzelm@49470
   155
wenzelm@49470
   156
  val default_thread_pool =
wenzelm@49470
   157
    scala.collection.parallel.ThreadPoolTasks.defaultThreadPool
wenzelm@43652
   158
}