--- 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 */
--- 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)
--- 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))
}
}
--- 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)
--- 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;
--- 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 _
+}
--- 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)
}