imitate exception ERROR of Isabelle/ML;
authorwenzelm
Mon Jul 04 13:43:10 2011 +0200 (2011-07-04)
changeset 43650f00da558b78e
parent 43649 a912f0b02359
child 43651 511df47bcadc
imitate exception ERROR of Isabelle/ML;
src/Pure/General/yxml.scala
src/Pure/PIDE/text.scala
src/Pure/System/cygwin.scala
src/Pure/System/gui_setup.scala
src/Pure/package.scala
src/Tools/jEdit/src/document_view.scala
     1.1 --- a/src/Pure/General/yxml.scala	Sun Jul 03 19:53:35 2011 +0200
     1.2 +++ b/src/Pure/General/yxml.scala	Mon Jul 04 13:43:10 2011 +0200
     1.3 @@ -144,12 +144,12 @@
     1.4    def parse_body_failsafe(source: CharSequence): XML.Body =
     1.5    {
     1.6      try { parse_body(source) }
     1.7 -    catch { case _: RuntimeException => List(markup_failsafe(source)) }
     1.8 +    catch { case ERROR(_) => List(markup_failsafe(source)) }
     1.9    }
    1.10  
    1.11    def parse_failsafe(source: CharSequence): XML.Tree =
    1.12    {
    1.13      try { parse(source) }
    1.14 -    catch { case _: RuntimeException => markup_failsafe(source) }
    1.15 +    catch { case ERROR(_) => markup_failsafe(source) }
    1.16    }
    1.17  }
     2.1 --- a/src/Pure/PIDE/text.scala	Sun Jul 03 19:53:35 2011 +0200
     2.2 +++ b/src/Pure/PIDE/text.scala	Mon Jul 04 13:43:10 2011 +0200
     2.3 @@ -46,7 +46,7 @@
     2.4  
     2.5      def try_restrict(that: Range): Option[Range] =
     2.6        try { Some (restrict(that)) }
     2.7 -      catch { case _: RuntimeException => None }
     2.8 +      catch { case ERROR(_) => None }
     2.9    }
    2.10  
    2.11  
    2.12 @@ -57,7 +57,7 @@
    2.13      def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
    2.14      def try_restrict(r: Text.Range): Option[Info[A]] =
    2.15        try { Some(Info(range.restrict(r), info)) }
    2.16 -      catch { case _: RuntimeException => None }
    2.17 +      catch { case ERROR(_) => None }
    2.18    }
    2.19  
    2.20  
     3.1 --- a/src/Pure/System/cygwin.scala	Sun Jul 03 19:53:35 2011 +0200
     3.2 +++ b/src/Pure/System/cygwin.scala	Mon Jul 04 13:43:10 2011 +0200
     3.3 @@ -115,7 +115,7 @@
     3.4      try {
     3.5        Download.file(parent, "Downloading", new URL("http://www.cygwin.com/setup.exe"), setup_exe)
     3.6      }
     3.7 -    catch { case _: RuntimeException => error("Failed to download Cygwin setup program") }
     3.8 +    catch { case ERROR(_) => error("Failed to download Cygwin setup program") }
     3.9  
    3.10      val (_, rc) = Standard_System.raw_exec(root, null, true,
    3.11          setup_exe.toString, "-R", root.toString, "-l", download.toString,
     4.1 --- a/src/Pure/System/gui_setup.scala	Sun Jul 03 19:53:35 2011 +0200
     4.2 +++ b/src/Pure/System/gui_setup.scala	Mon Jul 04 13:43:10 2011 +0200
     4.3 @@ -51,9 +51,7 @@
     4.4        if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
     4.5        text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
     4.6        text.append("Isabelle java: " + isabelle_system.this_java() + "\n")
     4.7 -    } catch {
     4.8 -      case e: RuntimeException => text.append(e.getMessage + "\n")
     4.9 -    }
    4.10 +    } catch { case ERROR(msg) => text.append(msg + "\n") }
    4.11  
    4.12      // reactions
    4.13      listenTo(ok)
     5.1 --- a/src/Pure/package.scala	Sun Jul 03 19:53:35 2011 +0200
     5.2 +++ b/src/Pure/package.scala	Mon Jul 04 13:43:10 2011 +0200
     5.3 @@ -6,6 +6,17 @@
     5.4  
     5.5  package object isabelle
     5.6  {
     5.7 -  def error(message: String): Nothing = throw new RuntimeException(message)
     5.8 +  object ERROR
     5.9 +  {
    5.10 +    def apply(message: String): Throwable = new RuntimeException(message)
    5.11 +    def unapply(exn: Throwable): Option[String] =
    5.12 +      exn match {
    5.13 +        case e: RuntimeException =>
    5.14 +          val msg = e.getMessage
    5.15 +          Some(if (msg == null) "" else msg)
    5.16 +        case _ => None
    5.17 +      }
    5.18 +  }
    5.19 +  def error(message: String): Nothing = throw ERROR(message)
    5.20  }
    5.21  
     6.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Jul 03 19:53:35 2011 +0200
     6.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Jul 04 13:43:10 2011 +0200
     6.3 @@ -78,7 +78,7 @@
     6.4        Swing_Thread.require()
     6.5        if (model.buffer == text_area.getBuffer) body
     6.6        else {
     6.7 -        Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model"))
     6.8 +        Log.log(Log.ERROR, this, ERROR("Inconsistent document model"))
     6.9          default
    6.10        }
    6.11      }