# HG changeset patch
# User wenzelm
# Date 1399313433 -7200
# Node ID d06ff36b4fa7301eb0365733a0aa87b133f84ee0
# Parent  1902d7c260174b6fccd175e183934ef0bfe5c2e1
expose interrupts more like ML version, but not in managed bash processes of Build;

diff -r 1902d7c26017 -r d06ff36b4fa7 src/Pure/System/isabelle_system.scala
--- 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)
     }
   }
diff -r 1902d7c26017 -r d06ff36b4fa7 src/Pure/Tools/build.scala
--- 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