# HG changeset patch # User wenzelm # Date 1219687277 -7200 # Node ID 6dd90ef9f9276674acad3a72f89d9a3e95fed91e # Parent 131f7ea9e6e6276bbc562c1bbfc7914758a47124 simplified exceptions: use plain error function / RuntimeException; diff -r 131f7ea9e6e6 -r 6dd90ef9f927 src/Pure/General/position.scala --- 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 } } } diff -r 131f7ea9e6e6 -r 6dd90ef9f927 src/Pure/General/symbol.scala --- 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))) } diff -r 131f7ea9e6e6 -r 6dd90ef9f927 src/Pure/General/yxml.scala --- 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>")))) } } diff -r 131f7ea9e6e6 -r 6dd90ef9f927 src/Pure/Tools/isabelle_process.scala --- 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 */ diff -r 131f7ea9e6e6 -r 6dd90ef9f927 src/Pure/Tools/isabelle_system.scala --- 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) }