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