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

     2.1 --- a/src/Pure/General/symbol.scala	Mon Aug 25 16:52:11 2008 +0200
     2.2 +++ b/src/Pure/General/symbol.scala	Mon Aug 25 20:01:17 2008 +0200
     2.3 @@ -81,8 +81,6 @@
     2.4  
     2.5    class Interpretation {
     2.6  
     2.7 -    class BadSymbol(val msg: String) extends Exception
     2.8 -
     2.9      private var symbols = new HashMap[String, HashMap[String, String]]
    2.10      private var decoder: Recoder = null
    2.11      private var encoder: Recoder = null
    2.12 @@ -98,7 +96,7 @@
    2.13      private val key_pattern = compile(""" (.+): """)
    2.14  
    2.15      private def read_line(line: String) = {
    2.16 -      def err() = throw new BadSymbol(line)
    2.17 +      def err() = error("Bad symbol specification (line " + line + ")")
    2.18  
    2.19        def read_props(props: List[String], tab: HashMap[String, String]): Unit = {
    2.20          props match {
    2.21 @@ -142,8 +140,8 @@
    2.22        val code =
    2.23          try { Integer.decode(props("code")).intValue }
    2.24          catch {
    2.25 -          case e: NoSuchElementException => throw new BadSymbol(symbol)
    2.26 -          case e: NumberFormatException => throw new BadSymbol(symbol)
    2.27 +          case _: NoSuchElementException => error("Missing code for symbol " + symbol)
    2.28 +          case _: NumberFormatException => error("Bad code for symbol " + symbol)
    2.29          }
    2.30        (symbol, new String(Character.toChars(code)))
    2.31      }

     3.1 --- a/src/Pure/General/yxml.scala	Mon Aug 25 16:52:11 2008 +0200
     3.2 +++ b/src/Pure/General/yxml.scala	Mon Aug 25 20:01:17 2008 +0200
     3.3 @@ -49,9 +49,7 @@
     3.4  
     3.5    /* parsing */
     3.6  
     3.7 -  class BadYXML(msg: String) extends Exception
     3.8 -
     3.9 -  private def err(msg: String) = throw new BadYXML(msg)
    3.10 +  private def err(msg: String) = error("Malformed YXML: " + msg)
    3.11    private def err_attribute() = err("bad attribute")
    3.12    private def err_element() = err("bad element")
    3.13    private def err_unbalanced(name: String) =
    3.14 @@ -115,7 +113,7 @@
    3.15    def parse_failsafe(source: CharSequence) = {
    3.16      try { parse(source) }
    3.17      catch {
    3.18 -      case e: BadYXML => XML.Elem (Markup.BAD, Nil,
    3.19 +      case _: RuntimeException => XML.Elem (Markup.BAD, Nil,
    3.20          List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
    3.21      }
    3.22    }

     4.1 --- a/src/Pure/Tools/isabelle_process.scala	Mon Aug 25 16:52:11 2008 +0200
     4.2 +++ b/src/Pure/Tools/isabelle_process.scala	Mon Aug 25 20:01:17 2008 +0200
     4.3 @@ -17,13 +17,6 @@
     4.4  
     4.5  object IsabelleProcess {
     4.6  
     4.7 -  /* exception */
     4.8 -
     4.9 -  class IsabelleProcessException(msg: String) extends Exception {
    4.10 -    override def toString = "IsabelleProcess: " + msg
    4.11 -  }
    4.12 -
    4.13 -
    4.14    /* results */
    4.15  
    4.16    object Kind extends Enumeration {
    4.17 @@ -120,7 +113,7 @@
    4.18    /* signals */
    4.19  
    4.20    def interrupt() = synchronized {
    4.21 -    if (proc == null) throw new IsabelleProcessException("Cannot interrupt: no process")
    4.22 +    if (proc == null) error("Cannot interrupt Isabelle: no process")
    4.23      if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
    4.24      else {
    4.25        try {
    4.26 @@ -129,12 +122,12 @@
    4.27          else
    4.28            put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
    4.29        }
    4.30 -      catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) }
    4.31 +      catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
    4.32      }
    4.33    }
    4.34  
    4.35    def kill() = synchronized {
    4.36 -    if (proc == 0) throw new IsabelleProcessException("Cannot kill: no process")
    4.37 +    if (proc == 0) error("Cannot kill Isabelle: no process")
    4.38      else {
    4.39        try_close()
    4.40        Thread.sleep(500)
    4.41 @@ -151,8 +144,8 @@
    4.42    private val output = new LinkedBlockingQueue[String]
    4.43  
    4.44    def output_raw(text: String) = synchronized {
    4.45 -    if (proc == null) throw new IsabelleProcessException("Cannot output: no process")
    4.46 -    if (closing) throw new IsabelleProcessException("Cannot output: already closing")
    4.47 +    if (proc == null) error("Cannot output to Isabelle: no process")
    4.48 +    if (closing) error("Cannot output to Isabelle: already closing")
    4.49      output.put(text)
    4.50    }
    4.51  
    4.52 @@ -177,7 +170,7 @@
    4.53    def try_close() = synchronized {
    4.54      if (proc != null && !closing) {
    4.55        try { close() }
    4.56 -      catch { case _: IsabelleProcessException => () }
    4.57 +      catch { case _: RuntimeException => }
    4.58      }
    4.59    }
    4.60  
    4.61 @@ -361,7 +354,9 @@
    4.62        proc = IsabelleSystem.exec(List(
    4.63          IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W") ++ args)
    4.64      }
    4.65 -    catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) }
    4.66 +    catch {
    4.67 +      case e: IOException => error("Failed to execute Isabelle process: " + e.getMessage)
    4.68 +    }
    4.69  
    4.70  
    4.71      /* control process via threads */

     5.1 --- a/src/Pure/Tools/isabelle_system.scala	Mon Aug 25 16:52:11 2008 +0200
     5.2 +++ b/src/Pure/Tools/isabelle_system.scala	Mon Aug 25 20:01:17 2008 +0200
     5.3 @@ -20,13 +20,9 @@
     5.4      if (value != null) value else ""
     5.5    }
     5.6  
     5.7 -  class BadVariable(val name: String) extends Exception {
     5.8 -    override def toString = "BadVariable: " + name
     5.9 -  }
    5.10 -
    5.11    def getenv_strict(name: String) = {
    5.12      val value = getenv(name)
    5.13 -    if (value != "") value else throw new BadVariable(name)
    5.14 +    if (value != "") value else error("Undefined environment variable: " + name)
    5.15    }
    5.16  
    5.17