# HG changeset patch
# User wenzelm
# Date 1309791105 -7200
# Node ID dcd0b667f73d607d2c67cc47533c2cc0a0212b1c
# Parent  511df47bcadc0ff0668fdc1775b353131b10c43b
pervasive Basic_Library in Scala;
tuned;

diff -r 511df47bcadc -r dcd0b667f73d src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Mon Jul 04 16:27:11 2011 +0200
+++ b/src/Pure/General/path.scala	Mon Jul 04 16:51:45 2011 +0200
@@ -19,7 +19,7 @@
   private case object Parent extends Elem
 
   private def err_elem(msg: String, s: String): Nothing =
-    error (msg + " path element specification: " + Library.quote(s))
+    error (msg + " path element specification: " + quote(s))
 
   private def check_elem(s: String): String =
     if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
@@ -27,7 +27,7 @@
       s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match {
         case Nil => s
         case bads =>
-          err_elem ("Illegal character(s) " + Library.commas_quote(bads.map(_.toString)) + " in", s)
+          err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s)
       }
 
   private def root_elem(s: String): Elem = Root(check_elem(s))
@@ -114,7 +114,7 @@
       case _ => elems.map(Path.implode_elem).reverse.mkString("/")
     }
 
-  override def toString: String = Library.quote(implode)
+  override def toString: String = quote(implode)
 
 
   /* base element */
diff -r 511df47bcadc -r dcd0b667f73d src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Jul 04 16:27:11 2011 +0200
+++ b/src/Pure/System/session.scala	Mon Jul 04 16:51:45 2011 +0200
@@ -154,7 +154,7 @@
     override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
     {
       val file = system.platform_file(dir + Thy_Header.thy_path(name))
-      if (!file.exists || !file.isFile) error("No such file: " + Library.quote(file.toString))
+      if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
       val text = Standard_System.read_file(file)
       val header = thy_header.read(text)
       (text, header)
diff -r 511df47bcadc -r dcd0b667f73d src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Jul 04 16:27:11 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Mon Jul 04 16:51:45 2011 +0200
@@ -119,6 +119,6 @@
     val header = read(source)
     val name1 = header.name
     if (name == name1) header
-    else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + Library.quote(name1))
+    else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + quote(name1))
   }
 }
diff -r 511df47bcadc -r dcd0b667f73d src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Mon Jul 04 16:27:11 2011 +0200
+++ b/src/Pure/Thy/thy_info.scala	Mon Jul 04 16:51:45 2011 +0200
@@ -12,7 +12,7 @@
   /* messages */
 
   private def show_path(names: List[String]): String =
-    names.map(Library.quote).mkString(" via ")
+    names.map(quote).mkString(" via ")
 
   private def cycle_msg(names: List[String]): String =
     "Cyclic dependency of " + show_path(names)
@@ -45,7 +45,7 @@
           catch {
             case ERROR(msg) =>
               cat_error(msg, "The error(s) above occurred while examining theory " +
-                Library.quote(name) + required_by("\n", initiators))
+                quote(name) + required_by("\n", initiators))
           }
         require_thys(name :: initiators, dir1,
           deps + (name -> Exn.Res(text, header)), header.imports)
diff -r 511df47bcadc -r dcd0b667f73d src/Pure/library.ML
--- a/src/Pure/library.ML	Mon Jul 04 16:27:11 2011 +0200
+++ b/src/Pure/library.ML	Mon Jul 04 16:51:45 2011 +0200
@@ -28,7 +28,7 @@
   val funpow: int -> ('a -> 'a) -> 'a -> 'a
   val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
 
-  (*errors*)
+  (*user errors*)
   exception ERROR of string
   val error: string -> 'a
   val cat_error: string -> string -> 'a
@@ -260,7 +260,7 @@
   | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
 
 
-(* errors *)
+(* user errors *)
 
 exception ERROR of string;
 fun error msg = raise ERROR msg;
diff -r 511df47bcadc -r dcd0b667f73d src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Jul 04 16:27:11 2011 +0200
+++ b/src/Pure/library.scala	Mon Jul 04 16:51:45 2011 +0200
@@ -18,6 +18,27 @@
 
 object Library
 {
+  /* user errors */
+
+  object ERROR
+  {
+    def apply(message: String): Throwable = new RuntimeException(message)
+    def unapply(exn: Throwable): Option[String] =
+      exn match {
+        case e: RuntimeException =>
+          val msg = e.getMessage
+          Some(if (msg == null) "" else msg)
+        case _ => None
+      }
+  }
+
+  def error(message: String): Nothing = throw ERROR(message)
+
+  def cat_error(msg1: String, msg2: String): Nothing =
+    if (msg1 == "") error(msg1)
+    else error(msg1 + "\n" + msg2)
+
+
   /* lists */
 
   def separate[A](s: A, list: List[A]): List[A] =
@@ -41,6 +62,37 @@
     }
 
 
+  /* iterate over chunks (cf. space_explode) */
+
+  def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
+  {
+    private val end = source.length
+    private def next_chunk(i: Int): Option[(CharSequence, Int)] =
+    {
+      if (i < end) {
+        var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
+        Some((source.subSequence(i + 1, j), j))
+      }
+      else None
+    }
+    private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
+
+    def hasNext(): Boolean = state.isDefined
+    def next(): CharSequence =
+      state match {
+        case Some((s, i)) => { state = next_chunk(i); s }
+        case None => Iterator.empty.next()
+      }
+  }
+
+  def first_line(source: CharSequence): String =
+  {
+    val lines = chunks(source)
+    if (lines.hasNext) lines.next.toString
+    else ""
+  }
+
+
   /* strings */
 
   def quote(s: String): String = "\"" + s + "\""
@@ -73,37 +125,6 @@
   }
 
 
-  /* iterate over chunks (cf. space_explode/split_lines in ML) */
-
-  def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
-  {
-    private val end = source.length
-    private def next_chunk(i: Int): Option[(CharSequence, Int)] =
-    {
-      if (i < end) {
-        var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
-        Some((source.subSequence(i + 1, j), j))
-      }
-      else None
-    }
-    private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
-
-    def hasNext(): Boolean = state.isDefined
-    def next(): CharSequence =
-      state match {
-        case Some((s, i)) => { state = next_chunk(i); s }
-        case None => Iterator.empty.next()
-      }
-  }
-
-  def first_line(source: CharSequence): String =
-  {
-    val lines = chunks(source)
-    if (lines.hasNext) lines.next.toString
-    else ""
-  }
-
-
   /* simple dialogs */
 
   private def simple_dialog(kind: Int, default_title: String)
@@ -160,3 +181,17 @@
     Exn.release(result)
   }
 }
+
+
+class Basic_Library
+{
+  val space_explode = Library.space_explode _
+
+  val quote = Library.quote _
+  val commas = Library.commas _
+  val commas_quote = Library.commas_quote _
+
+  val ERROR = Library.ERROR
+  val error = Library.error _
+  val cat_error = Library.cat_error _
+}
diff -r 511df47bcadc -r dcd0b667f73d src/Pure/package.scala
--- a/src/Pure/package.scala	Mon Jul 04 16:27:11 2011 +0200
+++ b/src/Pure/package.scala	Mon Jul 04 16:51:45 2011 +0200
@@ -4,26 +4,7 @@
 Toplevel isabelle package.
 */
 
-package object isabelle
+package object isabelle extends isabelle.Basic_Library
 {
-  /* errors */
-
-  object ERROR
-  {
-    def apply(message: String): Throwable = new RuntimeException(message)
-    def unapply(exn: Throwable): Option[String] =
-      exn match {
-        case e: RuntimeException =>
-          val msg = e.getMessage
-          Some(if (msg == null) "" else msg)
-        case _ => None
-      }
-  }
-
-  def error(message: String): Nothing = throw ERROR(message)
-
-  def cat_error(msg1: String, msg2: String): Nothing =
-    if (msg1 == "") error(msg1)
-    else error(msg1 + "\n" + msg2)
 }