1.1 --- a/src/Pure/library.scala	Mon Jul 04 16:27:11 2011 +0200
     1.2 +++ b/src/Pure/library.scala	Mon Jul 04 16:51:45 2011 +0200
     1.3 @@ -18,6 +18,27 @@
     1.4  
     1.5  object Library
     1.6  {
     1.7 +  /* user errors */
     1.8 +
     1.9 +  object ERROR
    1.10 +  {
    1.11 +    def apply(message: String): Throwable = new RuntimeException(message)
    1.12 +    def unapply(exn: Throwable): Option[String] =
    1.13 +      exn match {
    1.14 +        case e: RuntimeException =>
    1.15 +          val msg = e.getMessage
    1.16 +          Some(if (msg == null) "" else msg)
    1.17 +        case _ => None
    1.18 +      }
    1.19 +  }
    1.20 +
    1.21 +  def error(message: String): Nothing = throw ERROR(message)
    1.22 +
    1.23 +  def cat_error(msg1: String, msg2: String): Nothing =
    1.24 +    if (msg1 == "") error(msg1)
    1.25 +    else error(msg1 + "\n" + msg2)
    1.26 +
    1.27 +
    1.28    /* lists */
    1.29  
    1.30    def separate[A](s: A, list: List[A]): List[A] =
    1.31 @@ -41,39 +62,7 @@
    1.32      }
    1.33  
    1.34  
    1.35 -  /* strings */
    1.36 -
    1.37 -  def quote(s: String): String = "\"" + s + "\""
    1.38 -  def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
    1.39 -  def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"")
    1.40 -
    1.41 -
    1.42 -  /* reverse CharSequence */
    1.43 -
    1.44 -  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
    1.45 -  {
    1.46 -    require(0 <= start && start <= end && end <= text.length)
    1.47 -
    1.48 -    def this(text: CharSequence) = this(text, 0, text.length)
    1.49 -
    1.50 -    def length: Int = end - start
    1.51 -    def charAt(i: Int): Char = text.charAt(end - i - 1)
    1.52 -
    1.53 -    def subSequence(i: Int, j: Int): CharSequence =
    1.54 -      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
    1.55 -      else throw new IndexOutOfBoundsException
    1.56 -
    1.57 -    override def toString: String =
    1.58 -    {
    1.59 -      val buf = new StringBuilder(length)
    1.60 -      for (i <- 0 until length)
    1.61 -        buf.append(charAt(i))
    1.62 -      buf.toString
    1.63 -    }
    1.64 -  }
    1.65 -
    1.66 -
    1.67 -  /* iterate over chunks (cf. space_explode/split_lines in ML) */
    1.68 +  /* iterate over chunks (cf. space_explode) */
    1.69  
    1.70    def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
    1.71    {
    1.72 @@ -104,6 +93,38 @@
    1.73    }
    1.74  
    1.75  
    1.76 +  /* strings */
    1.77 +
    1.78 +  def quote(s: String): String = "\"" + s + "\""
    1.79 +  def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
    1.80 +  def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"")
    1.81 +
    1.82 +
    1.83 +  /* reverse CharSequence */
    1.84 +
    1.85 +  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
    1.86 +  {
    1.87 +    require(0 <= start && start <= end && end <= text.length)
    1.88 +
    1.89 +    def this(text: CharSequence) = this(text, 0, text.length)
    1.90 +
    1.91 +    def length: Int = end - start
    1.92 +    def charAt(i: Int): Char = text.charAt(end - i - 1)
    1.93 +
    1.94 +    def subSequence(i: Int, j: Int): CharSequence =
    1.95 +      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
    1.96 +      else throw new IndexOutOfBoundsException
    1.97 +
    1.98 +    override def toString: String =
    1.99 +    {
   1.100 +      val buf = new StringBuilder(length)
   1.101 +      for (i <- 0 until length)
   1.102 +        buf.append(charAt(i))
   1.103 +      buf.toString
   1.104 +    }
   1.105 +  }
   1.106 +
   1.107 +
   1.108    /* simple dialogs */
   1.109  
   1.110    private def simple_dialog(kind: Int, default_title: String)
   1.111 @@ -160,3 +181,17 @@
   1.112      Exn.release(result)
   1.113    }
   1.114  }
   1.115 +
   1.116 +
   1.117 +class Basic_Library
   1.118 +{
   1.119 +  val space_explode = Library.space_explode _
   1.120 +
   1.121 +  val quote = Library.quote _
   1.122 +  val commas = Library.commas _
   1.123 +  val commas_quote = Library.commas_quote _
   1.124 +
   1.125 +  val ERROR = Library.ERROR
   1.126 +  val error = Library.error _
   1.127 +  val cat_error = Library.cat_error _
   1.128 +}