more abstract Exn.Interrupt and POSIX return code;

--- a/src/Pure/Concurrent/simple_thread.scala	Wed Apr 23 11:40:42 2014 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala	Wed Apr 23 12:39:23 2014 +0200
@@ -15,10 +15,10 @@
 
 object Simple_Thread
 {
-  /* prending interrupts */
+  /* pending interrupts */
 
   def interrupted_exception(): Unit =
-    if (Thread.interrupted()) throw new InterruptedException
+    if (Thread.interrupted()) throw Exn.Interrupt()
 
 
   /* plain thread */

--- a/src/Pure/General/exn.ML	Wed Apr 23 11:40:42 2014 +0200
+++ b/src/Pure/General/exn.ML	Wed Apr 23 12:39:23 2014 +0200
@@ -19,6 +19,7 @@
   val interrupt_exn: 'a result
   val is_interrupt_exn: 'a result -> bool
   val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
+  val return_code: exn -> int -> int
   val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
   exception EXCEPTIONS of exn list
 end;
@@ -68,10 +69,13 @@
   Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
 
 
-(* POSIX process wrapper *)
+(* POSIX return code *)
+
+fun return_code exn rc =
+  if is_interrupt exn then (130: int) else rc;
 
 fun capture_exit rc f x =
-  f x handle exn => if is_interrupt exn then exit (130: int) else exit rc;
+  f x handle exn => exit (return_code exn rc);
 
 
 (* concatenated exceptions *)

--- a/src/Pure/General/exn.scala	Wed Apr 23 11:40:42 2014 +0200
+++ b/src/Pure/General/exn.scala	Wed Apr 23 12:39:23 2014 +0200
@@ -27,6 +27,26 @@
     }
 
 
+  /* interrupts */
+
+  def is_interrupt(exn: Throwable): Boolean =
+    exn.isInstanceOf[InterruptedException]
+
+  object Interrupt
+  {
+    def apply(): Throwable = new InterruptedException
+    def unapply(exn: Throwable): Boolean = is_interrupt(exn)
+
+    val return_code = 130
+  }
+
+
+  /* POSIX return code */
+
+  def return_code(exn: Throwable, rc: Int): Int =
+    if (is_interrupt(exn)) Interrupt.return_code else rc
+
+
   /* message */
 
   private val runtime_exception = Class.forName("java.lang.RuntimeException")
@@ -44,8 +64,6 @@
     else None
 
   def message(exn: Throwable): String =
-    user_message(exn) getOrElse
-      (if (exn.isInstanceOf[InterruptedException]) "Interrupt"
-       else exn.toString)
+    user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
 }
 

--- a/src/Pure/System/invoke_scala.scala	Wed Apr 23 11:40:42 2014 +0200
+++ b/src/Pure/System/invoke_scala.scala	Wed Apr 23 12:39:23 2014 +0200
@@ -58,7 +58,7 @@
         Exn.capture { f(arg) } match {
           case Exn.Res(null) => (Tag.NULL, "")
           case Exn.Res(res) => (Tag.OK, res)
-          case Exn.Exn(_: InterruptedException) => (Tag.INTERRUPT, "")
+          case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
           case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
         }
       case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))

--- a/src/Pure/System/isabelle_system.scala	Wed Apr 23 11:40:42 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Apr 23 12:39:23 2014 +0200
@@ -332,7 +332,7 @@
         kill_cmd(signal)
         kill_cmd("0") == 0
       }
-      catch { case _: InterruptedException => true }
+      catch { case Exn.Interrupt() => true }
     }
 
     private def multi_kill(signal: String): Boolean =
@@ -341,7 +341,7 @@
       var count = 10
       while (running && count > 0) {
         if (kill(signal)) {
-          try { Thread.sleep(100) } catch { case _: InterruptedException => }
+          try { Thread.sleep(100) } catch { case Exn.Interrupt() => }
           count -= 1
         }
         else running = false
@@ -481,7 +481,7 @@
 
       val rc =
         try { proc.join }
-        catch { case e: InterruptedException => proc.terminate; 130 }
+        catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
       Bash_Result(stdout.join, stderr.join, rc)
     }
   }

--- a/src/Pure/Tools/build.scala	Wed Apr 23 11:40:42 2014 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 23 12:39:23 2014 +0200
@@ -605,7 +605,7 @@
       args_file.delete
       timer.map(_.cancel())
 
-      if (res.rc == 130) {
+      if (res.rc == Exn.Interrupt.return_code) {
         if (timeout) res.add_err("*** Timeout").set_rc(1)
         else res.add_err("*** Interrupt")
       }
@@ -832,7 +832,7 @@
 
                 File.write(output_dir + log(name), Library.terminate_lines(res.out_lines))
                 progress.echo(name + " FAILED")
-                if (res.rc != 130) {
+                if (res.rc != Exn.Interrupt.return_code) {
                   progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
                   val lines = res.out_lines.filterNot(_.startsWith("\f"))
                   val tail = lines.drop(lines.length - 20 max 0)

--- a/src/Pure/Tools/main.scala	Wed Apr 23 11:40:42 2014 +0200
+++ b/src/Pure/Tools/main.scala	Wed Apr 23 12:39:23 2014 +0200
@@ -25,7 +25,7 @@
     def exit_error(exn: Throwable): Nothing =
     {
       GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
-      system_dialog.return_code(2)
+      system_dialog.return_code(Exn.return_code(exn, 2))
       system_dialog.join_exit
     }
 
@@ -60,7 +60,7 @@
                     build_heap = true, more_dirs = more_dirs,
                     system_mode = system_mode, sessions = List(session)))
               }
-              catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }
+              catch { case exn: Throwable => (Exn.message(exn) + "\n", Exn.return_code(exn, 2)) }
 
             system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
             system_dialog.return_code(rc)
@@ -155,7 +155,7 @@
       catch { case exn: Throwable => exit_error(exn) }
 
       if (system_dialog.stopped) {
-        system_dialog.return_code(130)
+        system_dialog.return_code(Exn.Interrupt.return_code)
         system_dialog.join_exit
       }
     }