1.1 --- a/src/Pure/General/path.scala	Mon Jul 04 16:27:11 2011 +0200
     1.2 +++ b/src/Pure/General/path.scala	Mon Jul 04 16:51:45 2011 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    private case object Parent extends Elem
     1.5  
     1.6    private def err_elem(msg: String, s: String): Nothing =
     1.7 -    error (msg + " path element specification: " + Library.quote(s))
     1.8 +    error (msg + " path element specification: " + quote(s))
     1.9  
    1.10    private def check_elem(s: String): String =
    1.11      if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
    1.12 @@ -27,7 +27,7 @@
    1.13        s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match {
    1.14          case Nil => s
    1.15          case bads =>
    1.16 -          err_elem ("Illegal character(s) " + Library.commas_quote(bads.map(_.toString)) + " in", s)
    1.17 +          err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s)
    1.18        }
    1.19  
    1.20    private def root_elem(s: String): Elem = Root(check_elem(s))
    1.21 @@ -114,7 +114,7 @@
    1.22        case _ => elems.map(Path.implode_elem).reverse.mkString("/")
    1.23      }
    1.24  
    1.25 -  override def toString: String = Library.quote(implode)
    1.26 +  override def toString: String = quote(implode)
    1.27  
    1.28  
    1.29    /* base element */

     2.1 --- a/src/Pure/System/session.scala	Mon Jul 04 16:27:11 2011 +0200
     2.2 +++ b/src/Pure/System/session.scala	Mon Jul 04 16:51:45 2011 +0200
     2.3 @@ -154,7 +154,7 @@
     2.4      override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
     2.5      {
     2.6        val file = system.platform_file(dir + Thy_Header.thy_path(name))
     2.7 -      if (!file.exists || !file.isFile) error("No such file: " + Library.quote(file.toString))
     2.8 +      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
     2.9        val text = Standard_System.read_file(file)
    2.10        val header = thy_header.read(text)
    2.11        (text, header)

     3.1 --- a/src/Pure/Thy/thy_header.scala	Mon Jul 04 16:27:11 2011 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Jul 04 16:51:45 2011 +0200
     3.3 @@ -119,6 +119,6 @@
     3.4      val header = read(source)
     3.5      val name1 = header.name
     3.6      if (name == name1) header
     3.7 -    else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + Library.quote(name1))
     3.8 +    else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + quote(name1))
     3.9    }
    3.10  }

     4.1 --- a/src/Pure/Thy/thy_info.scala	Mon Jul 04 16:27:11 2011 +0200
     4.2 +++ b/src/Pure/Thy/thy_info.scala	Mon Jul 04 16:51:45 2011 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4    /* messages */
     4.5  
     4.6    private def show_path(names: List[String]): String =
     4.7 -    names.map(Library.quote).mkString(" via ")
     4.8 +    names.map(quote).mkString(" via ")
     4.9  
    4.10    private def cycle_msg(names: List[String]): String =
    4.11      "Cyclic dependency of " + show_path(names)
    4.12 @@ -45,7 +45,7 @@
    4.13            catch {
    4.14              case ERROR(msg) =>
    4.15                cat_error(msg, "The error(s) above occurred while examining theory " +
    4.16 -                Library.quote(name) + required_by("\n", initiators))
    4.17 +                quote(name) + required_by("\n", initiators))
    4.18            }
    4.19          require_thys(name :: initiators, dir1,
    4.20            deps + (name -> Exn.Res(text, header)), header.imports)

     5.1 --- a/src/Pure/library.ML	Mon Jul 04 16:27:11 2011 +0200
     5.2 +++ b/src/Pure/library.ML	Mon Jul 04 16:51:45 2011 +0200
     5.3 @@ -28,7 +28,7 @@
     5.4    val funpow: int -> ('a -> 'a) -> 'a -> 'a
     5.5    val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
     5.6  
     5.7 -  (*errors*)
     5.8 +  (*user errors*)
     5.9    exception ERROR of string
    5.10    val error: string -> 'a
    5.11    val cat_error: string -> string -> 'a
    5.12 @@ -260,7 +260,7 @@
    5.13    | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
    5.14  
    5.15  
    5.16 -(* errors *)
    5.17 +(* user errors *)
    5.18  
    5.19  exception ERROR of string;
    5.20  fun error msg = raise ERROR msg;

     6.1 --- a/src/Pure/library.scala	Mon Jul 04 16:27:11 2011 +0200
     6.2 +++ b/src/Pure/library.scala	Mon Jul 04 16:51:45 2011 +0200
     6.3 @@ -18,6 +18,27 @@
     6.4  
     6.5  object Library
     6.6  {
     6.7 +  /* user errors */
     6.8 +
     6.9 +  object ERROR
    6.10 +  {
    6.11 +    def apply(message: String): Throwable = new RuntimeException(message)
    6.12 +    def unapply(exn: Throwable): Option[String] =
    6.13 +      exn match {
    6.14 +        case e: RuntimeException =>
    6.15 +          val msg = e.getMessage
    6.16 +          Some(if (msg == null) "" else msg)
    6.17 +        case _ => None
    6.18 +      }
    6.19 +  }
    6.20 +
    6.21 +  def error(message: String): Nothing = throw ERROR(message)
    6.22 +
    6.23 +  def cat_error(msg1: String, msg2: String): Nothing =
    6.24 +    if (msg1 == "") error(msg1)
    6.25 +    else error(msg1 + "\n" + msg2)
    6.26 +
    6.27 +
    6.28    /* lists */
    6.29  
    6.30    def separate[A](s: A, list: List[A]): List[A] =
    6.31 @@ -41,39 +62,7 @@
    6.32      }
    6.33  
    6.34  
    6.35 -  /* strings */
    6.36 -
    6.37 -  def quote(s: String): String = "\"" + s + "\""
    6.38 -  def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
    6.39 -  def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"")
    6.40 -
    6.41 -
    6.42 -  /* reverse CharSequence */
    6.43 -
    6.44 -  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
    6.45 -  {
    6.46 -    require(0 <= start && start <= end && end <= text.length)
    6.47 -
    6.48 -    def this(text: CharSequence) = this(text, 0, text.length)
    6.49 -
    6.50 -    def length: Int = end - start
    6.51 -    def charAt(i: Int): Char = text.charAt(end - i - 1)
    6.52 -
    6.53 -    def subSequence(i: Int, j: Int): CharSequence =
    6.54 -      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
    6.55 -      else throw new IndexOutOfBoundsException
    6.56 -
    6.57 -    override def toString: String =
    6.58 -    {
    6.59 -      val buf = new StringBuilder(length)
    6.60 -      for (i <- 0 until length)
    6.61 -        buf.append(charAt(i))
    6.62 -      buf.toString
    6.63 -    }
    6.64 -  }
    6.65 -
    6.66 -
    6.67 -  /* iterate over chunks (cf. space_explode/split_lines in ML) */
    6.68 +  /* iterate over chunks (cf. space_explode) */
    6.69  
    6.70    def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
    6.71    {
    6.72 @@ -104,6 +93,38 @@
    6.73    }
    6.74  
    6.75  
    6.76 +  /* strings */
    6.77 +
    6.78 +  def quote(s: String): String = "\"" + s + "\""
    6.79 +  def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
    6.80 +  def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"")
    6.81 +
    6.82 +
    6.83 +  /* reverse CharSequence */
    6.84 +
    6.85 +  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
    6.86 +  {
    6.87 +    require(0 <= start && start <= end && end <= text.length)
    6.88 +
    6.89 +    def this(text: CharSequence) = this(text, 0, text.length)
    6.90 +
    6.91 +    def length: Int = end - start
    6.92 +    def charAt(i: Int): Char = text.charAt(end - i - 1)
    6.93 +
    6.94 +    def subSequence(i: Int, j: Int): CharSequence =
    6.95 +      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
    6.96 +      else throw new IndexOutOfBoundsException
    6.97 +
    6.98 +    override def toString: String =
    6.99 +    {
   6.100 +      val buf = new StringBuilder(length)
   6.101 +      for (i <- 0 until length)
   6.102 +        buf.append(charAt(i))
   6.103 +      buf.toString
   6.104 +    }
   6.105 +  }
   6.106 +
   6.107 +
   6.108    /* simple dialogs */
   6.109  
   6.110    private def simple_dialog(kind: Int, default_title: String)
   6.111 @@ -160,3 +181,17 @@
   6.112      Exn.release(result)
   6.113    }
   6.114  }
   6.115 +
   6.116 +
   6.117 +class Basic_Library
   6.118 +{
   6.119 +  val space_explode = Library.space_explode _
   6.120 +
   6.121 +  val quote = Library.quote _
   6.122 +  val commas = Library.commas _
   6.123 +  val commas_quote = Library.commas_quote _
   6.124 +
   6.125 +  val ERROR = Library.ERROR
   6.126 +  val error = Library.error _
   6.127 +  val cat_error = Library.cat_error _
   6.128 +}

     7.1 --- a/src/Pure/package.scala	Mon Jul 04 16:27:11 2011 +0200
     7.2 +++ b/src/Pure/package.scala	Mon Jul 04 16:51:45 2011 +0200
     7.3 @@ -4,26 +4,7 @@
     7.4  Toplevel isabelle package.
     7.5  */
     7.6  
     7.7 -package object isabelle
     7.8 +package object isabelle extends isabelle.Basic_Library
     7.9  {
    7.10 -  /* errors */
    7.11 -
    7.12 -  object ERROR
    7.13 -  {
    7.14 -    def apply(message: String): Throwable = new RuntimeException(message)
    7.15 -    def unapply(exn: Throwable): Option[String] =
    7.16 -      exn match {
    7.17 -        case e: RuntimeException =>
    7.18 -          val msg = e.getMessage
    7.19 -          Some(if (msg == null) "" else msg)
    7.20 -        case _ => None
    7.21 -      }
    7.22 -  }
    7.23 -
    7.24 -  def error(message: String): Nothing = throw ERROR(message)
    7.25 -
    7.26 -  def cat_error(msg1: String, msg2: String): Nothing =
    7.27 -    if (msg1 == "") error(msg1)
    7.28 -    else error(msg1 + "\n" + msg2)
    7.29  }
    7.30