# HG changeset patch
# User wenzelm
# Date 1456862438 -3600
# Node ID 0e53fade87fe8dd2c20762f6b98c61b9c46cfe2b
# Parent  7187cb7a77c5501319578c30b58ee7e9d9639a04
clarified modules;

diff -r 7187cb7a77c5 -r 0e53fade87fe src/Pure/PIDE/document.scala
--- 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)
diff -r 7187cb7a77c5 -r 0e53fade87fe src/Pure/RAW/exn.ML
--- 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;
diff -r 7187cb7a77c5 -r 0e53fade87fe src/Pure/RAW/exn.scala
--- 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)
diff -r 7187cb7a77c5 -r 0e53fade87fe src/Pure/ROOT.scala
--- 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 _
 }
-
diff -r 7187cb7a77c5 -r 0e53fade87fe src/Pure/System/process_result.scala
--- 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 =
   {
diff -r 7187cb7a77c5 -r 0e53fade87fe src/Pure/library.scala
--- 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 _
-}