simplified exceptions: use plain error function / RuntimeException;

--- a/src/Pure/General/position.scala	Mon Aug 25 16:52:11 2008 +0200
+++ b/src/Pure/General/position.scala	Mon Aug 25 20:01:17 2008 +0200
@@ -22,7 +22,7 @@
       case None => None
       case Some(value) =>
         try { Some(Integer.parseInt(value)) }
-        catch { case e: NumberFormatException => None }
+        catch { case _: NumberFormatException => None }
     }
   }
 

--- a/src/Pure/General/symbol.scala	Mon Aug 25 16:52:11 2008 +0200
+++ b/src/Pure/General/symbol.scala	Mon Aug 25 20:01:17 2008 +0200
@@ -81,8 +81,6 @@
 
   class Interpretation {
 
-    class BadSymbol(val msg: String) extends Exception
-
     private var symbols = new HashMap[String, HashMap[String, String]]
     private var decoder: Recoder = null
     private var encoder: Recoder = null
@@ -98,7 +96,7 @@
     private val key_pattern = compile(""" (.+): """)
 
     private def read_line(line: String) = {
-      def err() = throw new BadSymbol(line)
+      def err() = error("Bad symbol specification (line " + line + ")")
 
       def read_props(props: List[String], tab: HashMap[String, String]): Unit = {
         props match {
@@ -142,8 +140,8 @@
       val code =
         try { Integer.decode(props("code")).intValue }
         catch {
-          case e: NoSuchElementException => throw new BadSymbol(symbol)
-          case e: NumberFormatException => throw new BadSymbol(symbol)
+          case _: NoSuchElementException => error("Missing code for symbol " + symbol)
+          case _: NumberFormatException => error("Bad code for symbol " + symbol)
         }
       (symbol, new String(Character.toChars(code)))
     }

--- a/src/Pure/General/yxml.scala	Mon Aug 25 16:52:11 2008 +0200
+++ b/src/Pure/General/yxml.scala	Mon Aug 25 20:01:17 2008 +0200
@@ -49,9 +49,7 @@
 
   /* parsing */
 
-  class BadYXML(msg: String) extends Exception
-
-  private def err(msg: String) = throw new BadYXML(msg)
+  private def err(msg: String) = error("Malformed YXML: " + msg)
   private def err_attribute() = err("bad attribute")
   private def err_element() = err("bad element")
   private def err_unbalanced(name: String) =
@@ -115,7 +113,7 @@
   def parse_failsafe(source: CharSequence) = {
     try { parse(source) }
     catch {
-      case e: BadYXML => XML.Elem (Markup.BAD, Nil,
+      case _: RuntimeException => XML.Elem (Markup.BAD, Nil,
         List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
     }
   }

--- a/src/Pure/Tools/isabelle_process.scala	Mon Aug 25 16:52:11 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.scala	Mon Aug 25 20:01:17 2008 +0200
@@ -17,13 +17,6 @@
 
 object IsabelleProcess {
 
-  /* exception */
-
-  class IsabelleProcessException(msg: String) extends Exception {
-    override def toString = "IsabelleProcess: " + msg
-  }
-
-
   /* results */
 
   object Kind extends Enumeration {
@@ -120,7 +113,7 @@
   /* signals */
 
   def interrupt() = synchronized {
-    if (proc == null) throw new IsabelleProcessException("Cannot interrupt: no process")
+    if (proc == null) error("Cannot interrupt Isabelle: no process")
     if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
     else {
       try {
@@ -129,12 +122,12 @@
         else
           put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
       }
-      catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) }
+      catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
     }
   }
 
   def kill() = synchronized {
-    if (proc == 0) throw new IsabelleProcessException("Cannot kill: no process")
+    if (proc == 0) error("Cannot kill Isabelle: no process")
     else {
       try_close()
       Thread.sleep(500)
@@ -151,8 +144,8 @@
   private val output = new LinkedBlockingQueue[String]
 
   def output_raw(text: String) = synchronized {
-    if (proc == null) throw new IsabelleProcessException("Cannot output: no process")
-    if (closing) throw new IsabelleProcessException("Cannot output: already closing")
+    if (proc == null) error("Cannot output to Isabelle: no process")
+    if (closing) error("Cannot output to Isabelle: already closing")
     output.put(text)
   }
 
@@ -177,7 +170,7 @@
   def try_close() = synchronized {
     if (proc != null && !closing) {
       try { close() }
-      catch { case _: IsabelleProcessException => () }
+      catch { case _: RuntimeException => }
     }
   }
 
@@ -361,7 +354,9 @@
       proc = IsabelleSystem.exec(List(
         IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W") ++ args)
     }
-    catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) }
+    catch {
+      case e: IOException => error("Failed to execute Isabelle process: " + e.getMessage)
+    }
 
 
     /* control process via threads */

--- a/src/Pure/Tools/isabelle_system.scala	Mon Aug 25 16:52:11 2008 +0200
+++ b/src/Pure/Tools/isabelle_system.scala	Mon Aug 25 20:01:17 2008 +0200
@@ -20,13 +20,9 @@
     if (value != null) value else ""
   }
 
-  class BadVariable(val name: String) extends Exception {
-    override def toString = "BadVariable: " + name
-  }
-
   def getenv_strict(name: String) = {
     val value = getenv(name)
-    if (value != "") value else throw new BadVariable(name)
+    if (value != "") value else error("Undefined environment variable: " + name)
   }