1.1 --- a/src/Pure/Tools/isabelle_process.scala	Mon Aug 25 16:52:11 2008 +0200
     1.2 +++ b/src/Pure/Tools/isabelle_process.scala	Mon Aug 25 20:01:17 2008 +0200
     1.3 @@ -17,13 +17,6 @@
     1.4  
     1.5  object IsabelleProcess {
     1.6  
     1.7 -  /* exception */
     1.8 -
     1.9 -  class IsabelleProcessException(msg: String) extends Exception {
    1.10 -    override def toString = "IsabelleProcess: " + msg
    1.11 -  }
    1.12 -
    1.13 -
    1.14    /* results */
    1.15  
    1.16    object Kind extends Enumeration {
    1.17 @@ -120,7 +113,7 @@
    1.18    /* signals */
    1.19  
    1.20    def interrupt() = synchronized {
    1.21 -    if (proc == null) throw new IsabelleProcessException("Cannot interrupt: no process")
    1.22 +    if (proc == null) error("Cannot interrupt Isabelle: no process")
    1.23      if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
    1.24      else {
    1.25        try {
    1.26 @@ -129,12 +122,12 @@
    1.27          else
    1.28            put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
    1.29        }
    1.30 -      catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) }
    1.31 +      catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
    1.32      }
    1.33    }
    1.34  
    1.35    def kill() = synchronized {
    1.36 -    if (proc == 0) throw new IsabelleProcessException("Cannot kill: no process")
    1.37 +    if (proc == 0) error("Cannot kill Isabelle: no process")
    1.38      else {
    1.39        try_close()
    1.40        Thread.sleep(500)
    1.41 @@ -151,8 +144,8 @@
    1.42    private val output = new LinkedBlockingQueue[String]
    1.43  
    1.44    def output_raw(text: String) = synchronized {
    1.45 -    if (proc == null) throw new IsabelleProcessException("Cannot output: no process")
    1.46 -    if (closing) throw new IsabelleProcessException("Cannot output: already closing")
    1.47 +    if (proc == null) error("Cannot output to Isabelle: no process")
    1.48 +    if (closing) error("Cannot output to Isabelle: already closing")
    1.49      output.put(text)
    1.50    }
    1.51  
    1.52 @@ -177,7 +170,7 @@
    1.53    def try_close() = synchronized {
    1.54      if (proc != null && !closing) {
    1.55        try { close() }
    1.56 -      catch { case _: IsabelleProcessException => () }
    1.57 +      catch { case _: RuntimeException => }
    1.58      }
    1.59    }
    1.60  
    1.61 @@ -361,7 +354,9 @@
    1.62        proc = IsabelleSystem.exec(List(
    1.63          IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W") ++ args)
    1.64      }
    1.65 -    catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) }
    1.66 +    catch {
    1.67 +      case e: IOException => error("Failed to execute Isabelle process: " + e.getMessage)
    1.68 +    }
    1.69  
    1.70  
    1.71      /* control process via threads */