imitate exception ERROR of Isabelle/ML;

--- a/src/Pure/General/yxml.scala	Sun Jul 03 19:53:35 2011 +0200
+++ b/src/Pure/General/yxml.scala	Mon Jul 04 13:43:10 2011 +0200
@@ -144,12 +144,12 @@
   def parse_body_failsafe(source: CharSequence): XML.Body =
   {
     try { parse_body(source) }
-    catch { case _: RuntimeException => List(markup_failsafe(source)) }
+    catch { case ERROR(_) => List(markup_failsafe(source)) }
   }
 
   def parse_failsafe(source: CharSequence): XML.Tree =
   {
     try { parse(source) }
-    catch { case _: RuntimeException => markup_failsafe(source) }
+    catch { case ERROR(_) => markup_failsafe(source) }
   }
 }

--- a/src/Pure/PIDE/text.scala	Sun Jul 03 19:53:35 2011 +0200
+++ b/src/Pure/PIDE/text.scala	Mon Jul 04 13:43:10 2011 +0200
@@ -46,7 +46,7 @@
 
     def try_restrict(that: Range): Option[Range] =
       try { Some (restrict(that)) }
-      catch { case _: RuntimeException => None }
+      catch { case ERROR(_) => None }
   }
 
 
@@ -57,7 +57,7 @@
     def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
     def try_restrict(r: Text.Range): Option[Info[A]] =
       try { Some(Info(range.restrict(r), info)) }
-      catch { case _: RuntimeException => None }
+      catch { case ERROR(_) => None }
   }
 
 

--- a/src/Pure/System/cygwin.scala	Sun Jul 03 19:53:35 2011 +0200
+++ b/src/Pure/System/cygwin.scala	Mon Jul 04 13:43:10 2011 +0200
@@ -115,7 +115,7 @@
     try {
       Download.file(parent, "Downloading", new URL("http://www.cygwin.com/setup.exe"), setup_exe)
     }
-    catch { case _: RuntimeException => error("Failed to download Cygwin setup program") }
+    catch { case ERROR(_) => error("Failed to download Cygwin setup program") }
 
     val (_, rc) = Standard_System.raw_exec(root, null, true,
         setup_exe.toString, "-R", root.toString, "-l", download.toString,

--- a/src/Pure/System/gui_setup.scala	Sun Jul 03 19:53:35 2011 +0200
+++ b/src/Pure/System/gui_setup.scala	Mon Jul 04 13:43:10 2011 +0200
@@ -51,9 +51,7 @@
       if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
       text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
       text.append("Isabelle java: " + isabelle_system.this_java() + "\n")
-    } catch {
-      case e: RuntimeException => text.append(e.getMessage + "\n")
-    }
+    } catch { case ERROR(msg) => text.append(msg + "\n") }
 
     // reactions
     listenTo(ok)

--- a/src/Pure/package.scala	Sun Jul 03 19:53:35 2011 +0200
+++ b/src/Pure/package.scala	Mon Jul 04 13:43:10 2011 +0200
@@ -6,6 +6,17 @@
 
 package object isabelle
 {
-  def error(message: String): Nothing = throw new RuntimeException(message)
+  object ERROR
+  {
+    def apply(message: String): Throwable = new RuntimeException(message)
+    def unapply(exn: Throwable): Option[String] =
+      exn match {
+        case e: RuntimeException =>
+          val msg = e.getMessage
+          Some(if (msg == null) "" else msg)
+        case _ => None
+      }
+  }
+  def error(message: String): Nothing = throw ERROR(message)
 }
 

--- a/src/Tools/jEdit/src/document_view.scala	Sun Jul 03 19:53:35 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Jul 04 13:43:10 2011 +0200
@@ -78,7 +78,7 @@
       Swing_Thread.require()
       if (model.buffer == text_area.getBuffer) body
       else {
-        Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model"))
+        Log.log(Log.ERROR, this, ERROR("Inconsistent document model"))
         default
       }
     }