expose interrupts more like ML version, but not in managed bash processes of Build;

--- a/src/Pure/System/isabelle_system.scala	Mon May 05 17:48:55 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon May 05 20:10:33 2014 +0200
@@ -440,7 +440,11 @@
     def err: String = cat_lines(err_lines)
     def add_err(s: String): Bash_Result = copy(err_lines = err_lines ::: List(s))
     def set_rc(i: Int): Bash_Result = copy(rc = i)
-    def check_error: Bash_Result = if (rc != 0) error(err) else this
+
+    def check_error: Bash_Result =
+      if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
+      else if (rc != 0) error(err)
+      else this
   }
 
   private class Limited_Progress(proc: Managed_Process, progress_limit: Option[Long])
@@ -459,7 +463,8 @@
   def bash_env(cwd: JFile, env: Map[String, String], script: String,
     progress_stdout: String => Unit = (_: String) => (),
     progress_stderr: String => Unit = (_: String) => (),
-    progress_limit: Option[Long] = None): Bash_Result =
+    progress_limit: Option[Long] = None,
+    strict: Boolean = true): Bash_Result =
   {
     with_tmp_file("isabelle_script") { script_file =>
       File.write(script_file, script)
@@ -479,6 +484,8 @@
       val rc =
         try { proc.join }
         catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
+      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
+
       Bash_Result(stdout.join, stderr.join, rc)
     }
   }

--- a/src/Pure/Tools/build.scala	Mon May 05 17:48:55 2014 +0200
+++ b/src/Pure/Tools/build.scala	Mon May 05 20:10:33 2014 +0200
@@ -599,7 +599,8 @@
             info.options.int("process_output_limit") match {
               case 0 => None
               case m => Some(m * 1000000L)
-            })
+            },
+          strict = false)
       }
 
     def terminate: Unit = thread.interrupt