expose interrupts more like ML version, but not in managed bash processes of Build;
authorwenzelm
Mon May 05 20:10:33 2014 +0200 (2014-05-05)
changeset 56871d06ff36b4fa7
parent 56870 1902d7c26017
child 56872 1435f0c771dc
expose interrupts more like ML version, but not in managed bash processes of Build;
src/Pure/System/isabelle_system.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/System/isabelle_system.scala	Mon May 05 17:48:55 2014 +0200
     1.2 +++ b/src/Pure/System/isabelle_system.scala	Mon May 05 20:10:33 2014 +0200
     1.3 @@ -440,7 +440,11 @@
     1.4      def err: String = cat_lines(err_lines)
     1.5      def add_err(s: String): Bash_Result = copy(err_lines = err_lines ::: List(s))
     1.6      def set_rc(i: Int): Bash_Result = copy(rc = i)
     1.7 -    def check_error: Bash_Result = if (rc != 0) error(err) else this
     1.8 +
     1.9 +    def check_error: Bash_Result =
    1.10 +      if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
    1.11 +      else if (rc != 0) error(err)
    1.12 +      else this
    1.13    }
    1.14  
    1.15    private class Limited_Progress(proc: Managed_Process, progress_limit: Option[Long])
    1.16 @@ -459,7 +463,8 @@
    1.17    def bash_env(cwd: JFile, env: Map[String, String], script: String,
    1.18      progress_stdout: String => Unit = (_: String) => (),
    1.19      progress_stderr: String => Unit = (_: String) => (),
    1.20 -    progress_limit: Option[Long] = None): Bash_Result =
    1.21 +    progress_limit: Option[Long] = None,
    1.22 +    strict: Boolean = true): Bash_Result =
    1.23    {
    1.24      with_tmp_file("isabelle_script") { script_file =>
    1.25        File.write(script_file, script)
    1.26 @@ -479,6 +484,8 @@
    1.27        val rc =
    1.28          try { proc.join }
    1.29          catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
    1.30 +      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
    1.31 +
    1.32        Bash_Result(stdout.join, stderr.join, rc)
    1.33      }
    1.34    }
     2.1 --- a/src/Pure/Tools/build.scala	Mon May 05 17:48:55 2014 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Mon May 05 20:10:33 2014 +0200
     2.3 @@ -599,7 +599,8 @@
     2.4              info.options.int("process_output_limit") match {
     2.5                case 0 => None
     2.6                case m => Some(m * 1000000L)
     2.7 -            })
     2.8 +            },
     2.9 +          strict = false)
    2.10        }
    2.11  
    2.12      def terminate: Unit = thread.interrupt