tuned signature;

--- a/src/Pure/Concurrent/simple_thread.scala	Sun May 04 21:35:04 2014 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala	Mon May 05 09:24:34 2014 +0200
@@ -16,12 +16,6 @@
 
 object Simple_Thread
 {
-  /* pending interrupts */
-
-  def interrupted_exception(): Unit =
-    if (Thread.interrupted()) throw Exn.Interrupt()
-
-
   /* plain thread */
 
   def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =

--- a/src/Pure/General/exn.scala	Sun May 04 21:35:04 2014 +0200
+++ b/src/Pure/General/exn.scala	Mon May 05 09:24:34 2014 +0200
@@ -45,6 +45,8 @@
     def apply(): Throwable = new InterruptedException
     def unapply(exn: Throwable): Boolean = is_interrupt(exn)
 
+    def expose(): Unit = if (Thread.interrupted()) throw apply()
+
     val return_code = 130
   }
 

--- a/src/Pure/System/interrupt.scala	Sun May 04 21:35:04 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-/*  Title:      Pure/System/interrupt.scala
-    Author:     Makarius
-
-Support for POSIX interrupts (bypassed on Windows).
-*/
-
-package isabelle
-
-
-import sun.misc.{Signal, SignalHandler}
-
-
-object Interrupt
-{
-  def handler[A](h: => Unit)(e: => A): A =
-  {
-    val SIGINT = new Signal("INT")
-    val new_handler = new SignalHandler { def handle(s: Signal) { h } }
-    val old_handler = Signal.handle(SIGINT, new_handler)
-    try { e } finally { Signal.handle(SIGINT, old_handler) }
-  }
-
-  def exception[A](e: => A): A =
-  {
-    val thread = Thread.currentThread
-    handler { thread.interrupt } { e }
-  }
-}
-

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/posix_interrupt.scala	Mon May 05 09:24:34 2014 +0200
@@ -0,0 +1,29 @@
+/*  Title:      Pure/System/interrupt.scala
+    Author:     Makarius
+
+Support for POSIX interrupts (bypassed on Windows).
+*/
+
+package isabelle
+
+
+import sun.misc.{Signal, SignalHandler}
+
+
+object POSIX_Interrupt
+{
+  def handler[A](h: => Unit)(e: => A): A =
+  {
+    val SIGINT = new Signal("INT")
+    val new_handler = new SignalHandler { def handle(s: Signal) { h } }
+    val old_handler = Signal.handle(SIGINT, new_handler)
+    try { e } finally { Signal.handle(SIGINT, old_handler) }
+  }
+
+  def exception[A](e: => A): A =
+  {
+    val thread = Thread.currentThread
+    handler { thread.interrupt } { e }
+  }
+}
+

--- a/src/Pure/Tools/build.scala	Sun May 04 21:35:04 2014 +0200
+++ b/src/Pure/Tools/build.scala	Mon May 05 09:24:34 2014 +0200
@@ -37,7 +37,7 @@
       if (verbose) echo(session + ": theory " + theory)
 
     @volatile private var is_stopped = false
-    def interrupt_handler[A](e: => A): A = Interrupt.handler { is_stopped = true } { e }
+    def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { is_stopped = true } { e }
     override def stopped: Boolean =
     {
       if (Thread.interrupted) is_stopped = true

--- a/src/Pure/build-jars	Sun May 04 21:35:04 2014 +0200
+++ b/src/Pure/build-jars	Mon May 05 09:24:34 2014 +0200
@@ -67,7 +67,6 @@
   PIDE/xml.scala
   PIDE/yxml.scala
   System/command_line.scala
-  System/interrupt.scala
   System/invoke_scala.scala
   System/isabelle_charset.scala
   System/isabelle_font.scala
@@ -75,6 +74,7 @@
   System/isabelle_system.scala
   System/options.scala
   System/platform.scala
+  System/posix_interrupt.scala
   System/system_channel.scala
   System/utf8.scala
   Thy/html.scala

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun May 04 21:35:04 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon May 05 09:24:34 2014 +0200
@@ -124,7 +124,7 @@
           val (text, rendering) =
             try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
             catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
-          Simple_Thread.interrupted_exception()
+          Exn.Interrupt.expose()
 
           Swing_Thread.later {
             current_rendering = rendering