--- a/src/Pure/PIDE/document.scala Tue Mar 01 20:51:38 2016 +0100
+++ b/src/Pure/PIDE/document.scala Tue Mar 01 21:00:38 2016 +0100
@@ -88,7 +88,7 @@
def error(msg: String): Header = copy(errors = errors ::: List(msg))
def cat_errors(msg2: String): Header =
- copy(errors = errors.map(msg1 => Library.cat_message(msg1, msg2)))
+ copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2)))
}
val no_header = Header(Nil, Nil, Nil)
--- a/src/Pure/RAW/exn.ML Tue Mar 01 20:51:38 2016 +0100
+++ b/src/Pure/RAW/exn.ML Tue Mar 01 21:00:38 2016 +0100
@@ -36,6 +36,17 @@
structure Exn: EXN =
struct
+(* user errors *)
+
+exception ERROR of string;
+
+fun error msg = raise ERROR msg;
+
+fun cat_error "" msg = error msg
+ | cat_error msg "" = error msg
+ | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
+
+
(* exceptions as values *)
datatype 'a result =
@@ -94,17 +105,6 @@
exception EXCEPTIONS of exn list;
-
-(* user errors *)
-
-exception ERROR of string;
-
-fun error msg = raise ERROR msg;
-
-fun cat_error "" msg = error msg
- | cat_error msg "" = error msg
- | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
-
end;
datatype illegal = Interrupt;
--- a/src/Pure/RAW/exn.scala Tue Mar 01 20:51:38 2016 +0100
+++ b/src/Pure/RAW/exn.scala Tue Mar 01 21:00:38 2016 +0100
@@ -10,6 +10,37 @@
object Exn
{
+ /* user errors */
+
+ class User_Error(message: String) extends RuntimeException(message)
+ {
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: User_Error => message == other.getMessage
+ case _ => false
+ }
+ override def hashCode: Int = message.hashCode
+
+ override def toString: String = "ERROR(" + message + ")"
+ }
+
+ object ERROR
+ {
+ def apply(message: String): User_Error = new User_Error(message)
+ def unapply(exn: Throwable): Option[String] = user_message(exn)
+ }
+
+ def error(message: String): Nothing = throw ERROR(message)
+
+ def cat_message(msg1: String, msg2: String): String =
+ if (msg1 == "") msg2
+ else if (msg2 == "") msg1
+ else msg1 + "\n" + msg2
+
+ def cat_error(msg1: String, msg2: String): Nothing =
+ error(cat_message(msg1, msg2))
+
+
/* exceptions as values */
sealed abstract class Result[A]
@@ -88,7 +119,7 @@
def user_message(exn: Throwable): Option[String] =
if (exn.getClass == classOf[RuntimeException] ||
- exn.getClass == classOf[Library.User_Error])
+ exn.getClass == classOf[User_Error])
{
val msg = exn.getMessage
Some(if (msg == null || msg == "") "Error" else msg)
--- a/src/Pure/ROOT.scala Tue Mar 01 20:51:38 2016 +0100
+++ b/src/Pure/ROOT.scala Tue Mar 01 21:00:38 2016 +0100
@@ -5,7 +5,7 @@
Root of isabelle package.
*/
-package object isabelle extends isabelle.Basic_Library
+package object isabelle
{
object Distribution /*filled-in by makedist*/
{
@@ -13,5 +13,15 @@
val is_identified = false
val is_official = false
}
+
+ val ERROR = Exn.ERROR
+ val error = Exn.error _
+ val cat_error = Exn.cat_error _
+
+ val space_explode = Library.space_explode _
+ val split_lines = Library.split_lines _
+ val cat_lines = Library.cat_lines _
+ val quote = Library.quote _
+ val commas = Library.commas _
+ val commas_quote = Library.commas_quote _
}
-
--- a/src/Pure/System/process_result.scala Tue Mar 01 20:51:38 2016 +0100
+++ b/src/Pure/System/process_result.scala Tue Mar 01 21:00:38 2016 +0100
@@ -24,7 +24,7 @@
def check: Process_Result =
if (ok) this
else if (interrupted) throw Exn.Interrupt()
- else Library.error(err)
+ else Exn.error(err)
def print: Process_Result =
{
--- a/src/Pure/library.scala Tue Mar 01 20:51:38 2016 +0100
+++ b/src/Pure/library.scala Tue Mar 01 21:00:38 2016 +0100
@@ -14,37 +14,6 @@
object Library
{
- /* user errors */
-
- class User_Error(message: String) extends RuntimeException(message)
- {
- override def equals(that: Any): Boolean =
- that match {
- case other: User_Error => message == other.getMessage
- case _ => false
- }
- override def hashCode: Int = message.hashCode
-
- override def toString: String = "ERROR(" + message + ")"
- }
-
- object ERROR
- {
- def apply(message: String): User_Error = new User_Error(message)
- def unapply(exn: Throwable): Option[String] = Exn.user_message(exn)
- }
-
- def error(message: String): Nothing = throw ERROR(message)
-
- def cat_message(msg1: String, msg2: String): String =
- if (msg1 == "") msg2
- else if (msg2 == "") msg1
- else msg1 + "\n" + msg2
-
- def cat_error(msg1: String, msg2: String): Nothing =
- error(cat_message(msg1, msg2))
-
-
/* integers */
private val small_int = 10000
@@ -215,18 +184,3 @@
def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
}
-
-
-class Basic_Library
-{
- val ERROR = Library.ERROR
- val error = Library.error _
- val cat_error = Library.cat_error _
-
- val space_explode = Library.space_explode _
- val split_lines = Library.split_lines _
- val cat_lines = Library.cat_lines _
- val quote = Library.quote _
- val commas = Library.commas _
- val commas_quote = Library.commas_quote _
-}