src/Pure/library.scala
author wenzelm
Fri Oct 07 21:16:48 2016 +0200 (2016-10-07)
changeset 64092 95469c544b82
parent 64063 2c5039363ea3
child 64207 ad15c2f478b5
permissions -rw-r--r--
accept obscure timezone used in 2011;
     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.annotation.tailrec
    12 import scala.collection.mutable
    13 import scala.util.matching.Regex
    14 
    15 
    16 object Library
    17 {
    18   /* resource management */
    19 
    20   def using[A <: { def close() }, B](x: A)(f: A => B): B =
    21   {
    22     import scala.language.reflectiveCalls
    23 
    24     try { f(x) }
    25     finally { if (x != null) x.close() }
    26   }
    27 
    28 
    29   /* integers */
    30 
    31   private val small_int = 10000
    32   private lazy val small_int_table =
    33   {
    34     val array = new Array[String](small_int)
    35     for (i <- 0 until small_int) array(i) = i.toString
    36     array
    37   }
    38 
    39   def is_small_int(s: String): Boolean =
    40   {
    41     val len = s.length
    42     1 <= len && len <= 4 &&
    43     s.forall(c => '0' <= c && c <= '9') &&
    44     (len == 1 || s(0) != '0')
    45   }
    46 
    47   def signed_string_of_long(i: Long): String =
    48     if (0 <= i && i < small_int) small_int_table(i.toInt)
    49     else i.toString
    50 
    51   def signed_string_of_int(i: Int): String =
    52     if (0 <= i && i < small_int) small_int_table(i)
    53     else i.toString
    54 
    55 
    56   /* separated chunks */
    57 
    58   def separate[A](s: A, list: List[A]): List[A] =
    59   {
    60     val result = new mutable.ListBuffer[A]
    61     var first = true
    62     for (x <- list) {
    63       if (first) {
    64         first = false
    65         result += x
    66       }
    67       else {
    68         result += s
    69         result += x
    70       }
    71     }
    72     result.toList
    73   }
    74 
    75   def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] =
    76     new Iterator[CharSequence] {
    77       private val end = source.length
    78       private def next_chunk(i: Int): Option[(CharSequence, Int)] =
    79       {
    80         if (i < end) {
    81           var j = i; do j += 1 while (j < end && !sep(source.charAt(j)))
    82           Some((source.subSequence(i + 1, j), j))
    83         }
    84         else None
    85       }
    86       private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
    87 
    88       def hasNext(): Boolean = state.isDefined
    89       def next(): CharSequence =
    90         state match {
    91           case Some((s, i)) => state = next_chunk(i); s
    92           case None => Iterator.empty.next()
    93         }
    94     }
    95 
    96   def space_explode(sep: Char, str: String): List[String] =
    97     separated_chunks(_ == sep, str).map(_.toString).toList
    98 
    99 
   100   /* lines */
   101 
   102   def terminate_lines(lines: TraversableOnce[String]): String = lines.mkString("", "\n", "\n")
   103 
   104   def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
   105 
   106   def split_lines(str: String): List[String] = space_explode('\n', str)
   107 
   108   def prefix_lines(prfx: String, str: String): String =
   109     if (str == "") str
   110     else cat_lines(split_lines(str).map(s => prfx + s))
   111 
   112   def first_line(source: CharSequence): String =
   113   {
   114     val lines = separated_chunks(_ == '\n', source)
   115     if (lines.hasNext) lines.next.toString
   116     else ""
   117   }
   118 
   119 
   120   /* strings */
   121 
   122   def try_unprefix(prfx: String, s: String): Option[String] =
   123     if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
   124 
   125   def try_unsuffix(sffx: String, s: String): Option[String] =
   126     if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None
   127 
   128   def trim_line(s: String): String =
   129     if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
   130     else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
   131     else s
   132 
   133   def trim_split_lines(s: String): List[String] =
   134     split_lines(trim_line(s)).map(trim_line(_))
   135 
   136 
   137   /* quote */
   138 
   139   def quote(s: String): String = "\"" + s + "\""
   140 
   141   def try_unquote(s: String): Option[String] =
   142     if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1))
   143     else None
   144 
   145   def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s
   146 
   147   def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
   148   def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
   149 
   150 
   151   /* CharSequence */
   152 
   153   class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
   154   {
   155     require(0 <= start && start <= end && end <= text.length)
   156 
   157     def this(text: CharSequence) = this(text, 0, text.length)
   158 
   159     def length: Int = end - start
   160     def charAt(i: Int): Char = text.charAt(end - i - 1)
   161 
   162     def subSequence(i: Int, j: Int): CharSequence =
   163       if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
   164       else throw new IndexOutOfBoundsException
   165 
   166     override def toString: String =
   167     {
   168       val buf = new StringBuilder(length)
   169       for (i <- 0 until length)
   170         buf.append(charAt(i))
   171       buf.toString
   172     }
   173   }
   174 
   175   class Line_Termination(text: CharSequence) extends CharSequence
   176   {
   177     def length: Int = text.length + 1
   178     def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i)
   179     def subSequence(i: Int, j: Int): CharSequence =
   180       if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1))
   181       else text.subSequence(i, j)
   182     override def toString: String = text.toString + "\n"
   183   }
   184 
   185 
   186   /* regular expressions */
   187 
   188   def make_regex(s: String): Option[Regex] =
   189     try { Some(new Regex(s)) } catch { case ERROR(_) => None }
   190 
   191 
   192   /* lists */
   193 
   194   def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
   195     (xs.takeWhile(pred), xs.dropWhile(pred))
   196 
   197   def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
   198   def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   199   def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   200   def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
   201 
   202   def merge[A](xs: List[A], ys: List[A]): List[A] =
   203     if (xs.eq(ys)) xs
   204     else if (xs.isEmpty) ys
   205     else ys.foldRight(xs)(Library.insert(_)(_))
   206 
   207   def distinct[A](xs: List[A]): List[A] =
   208   {
   209     val result = new mutable.ListBuffer[A]
   210     xs.foreach(x => if (!result.contains(x)) result += x)
   211     result.toList
   212   }
   213 
   214   def duplicates[A](lst: List[A]): List[A] =
   215   {
   216     val result = new mutable.ListBuffer[A]
   217     @tailrec def dups(rest: List[A]): Unit =
   218       rest match {
   219         case Nil =>
   220         case x :: xs =>
   221           if (!result.contains(x) && xs.contains(x)) result += x
   222           dups(xs)
   223       }
   224     dups(lst)
   225     result.toList
   226   }
   227 }