1.1 --- a/src/Pure/Concurrent/simple_thread.scala Wed Apr 23 11:40:42 2014 +0200
1.2 +++ b/src/Pure/Concurrent/simple_thread.scala Wed Apr 23 12:39:23 2014 +0200
1.3 @@ -15,10 +15,10 @@
1.4
1.5 object Simple_Thread
1.6 {
1.7 - /* prending interrupts */
1.8 + /* pending interrupts */
1.9
1.10 def interrupted_exception(): Unit =
1.11 - if (Thread.interrupted()) throw new InterruptedException
1.12 + if (Thread.interrupted()) throw Exn.Interrupt()
1.13
1.14
1.15 /* plain thread */
2.1 --- a/src/Pure/General/exn.ML Wed Apr 23 11:40:42 2014 +0200
2.2 +++ b/src/Pure/General/exn.ML Wed Apr 23 12:39:23 2014 +0200
2.3 @@ -19,6 +19,7 @@
2.4 val interrupt_exn: 'a result
2.5 val is_interrupt_exn: 'a result -> bool
2.6 val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
2.7 + val return_code: exn -> int -> int
2.8 val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
2.9 exception EXCEPTIONS of exn list
2.10 end;
2.11 @@ -68,10 +69,13 @@
2.12 Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
2.13
2.14
2.15 -(* POSIX process wrapper *)
2.16 +(* POSIX return code *)
2.17 +
2.18 +fun return_code exn rc =
2.19 + if is_interrupt exn then (130: int) else rc;
2.20
2.21 fun capture_exit rc f x =
2.22 - f x handle exn => if is_interrupt exn then exit (130: int) else exit rc;
2.23 + f x handle exn => exit (return_code exn rc);
2.24
2.25
2.26 (* concatenated exceptions *)
3.1 --- a/src/Pure/General/exn.scala Wed Apr 23 11:40:42 2014 +0200
3.2 +++ b/src/Pure/General/exn.scala Wed Apr 23 12:39:23 2014 +0200
3.3 @@ -27,6 +27,26 @@
3.4 }
3.5
3.6
3.7 + /* interrupts */
3.8 +
3.9 + def is_interrupt(exn: Throwable): Boolean =
3.10 + exn.isInstanceOf[InterruptedException]
3.11 +
3.12 + object Interrupt
3.13 + {
3.14 + def apply(): Throwable = new InterruptedException
3.15 + def unapply(exn: Throwable): Boolean = is_interrupt(exn)
3.16 +
3.17 + val return_code = 130
3.18 + }
3.19 +
3.20 +
3.21 + /* POSIX return code */
3.22 +
3.23 + def return_code(exn: Throwable, rc: Int): Int =
3.24 + if (is_interrupt(exn)) Interrupt.return_code else rc
3.25 +
3.26 +
3.27 /* message */
3.28
3.29 private val runtime_exception = Class.forName("java.lang.RuntimeException")
3.30 @@ -44,8 +64,6 @@
3.31 else None
3.32
3.33 def message(exn: Throwable): String =
3.34 - user_message(exn) getOrElse
3.35 - (if (exn.isInstanceOf[InterruptedException]) "Interrupt"
3.36 - else exn.toString)
3.37 + user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
3.38 }
3.39
4.1 --- a/src/Pure/System/invoke_scala.scala Wed Apr 23 11:40:42 2014 +0200
4.2 +++ b/src/Pure/System/invoke_scala.scala Wed Apr 23 12:39:23 2014 +0200
4.3 @@ -58,7 +58,7 @@
4.4 Exn.capture { f(arg) } match {
4.5 case Exn.Res(null) => (Tag.NULL, "")
4.6 case Exn.Res(res) => (Tag.OK, res)
4.7 - case Exn.Exn(_: InterruptedException) => (Tag.INTERRUPT, "")
4.8 + case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
4.9 case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
4.10 }
4.11 case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
5.1 --- a/src/Pure/System/isabelle_system.scala Wed Apr 23 11:40:42 2014 +0200
5.2 +++ b/src/Pure/System/isabelle_system.scala Wed Apr 23 12:39:23 2014 +0200
5.3 @@ -332,7 +332,7 @@
5.4 kill_cmd(signal)
5.5 kill_cmd("0") == 0
5.6 }
5.7 - catch { case _: InterruptedException => true }
5.8 + catch { case Exn.Interrupt() => true }
5.9 }
5.10
5.11 private def multi_kill(signal: String): Boolean =
5.12 @@ -341,7 +341,7 @@
5.13 var count = 10
5.14 while (running && count > 0) {
5.15 if (kill(signal)) {
5.16 - try { Thread.sleep(100) } catch { case _: InterruptedException => }
5.17 + try { Thread.sleep(100) } catch { case Exn.Interrupt() => }
5.18 count -= 1
5.19 }
5.20 else running = false
5.21 @@ -481,7 +481,7 @@
5.22
5.23 val rc =
5.24 try { proc.join }
5.25 - catch { case e: InterruptedException => proc.terminate; 130 }
5.26 + catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
5.27 Bash_Result(stdout.join, stderr.join, rc)
5.28 }
5.29 }
6.1 --- a/src/Pure/Tools/build.scala Wed Apr 23 11:40:42 2014 +0200
6.2 +++ b/src/Pure/Tools/build.scala Wed Apr 23 12:39:23 2014 +0200
6.3 @@ -605,7 +605,7 @@
6.4 args_file.delete
6.5 timer.map(_.cancel())
6.6
6.7 - if (res.rc == 130) {
6.8 + if (res.rc == Exn.Interrupt.return_code) {
6.9 if (timeout) res.add_err("*** Timeout").set_rc(1)
6.10 else res.add_err("*** Interrupt")
6.11 }
6.12 @@ -832,7 +832,7 @@
6.13
6.14 File.write(output_dir + log(name), Library.terminate_lines(res.out_lines))
6.15 progress.echo(name + " FAILED")
6.16 - if (res.rc != 130) {
6.17 + if (res.rc != Exn.Interrupt.return_code) {
6.18 progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
6.19 val lines = res.out_lines.filterNot(_.startsWith("\f"))
6.20 val tail = lines.drop(lines.length - 20 max 0)
7.1 --- a/src/Pure/Tools/main.scala Wed Apr 23 11:40:42 2014 +0200
7.2 +++ b/src/Pure/Tools/main.scala Wed Apr 23 12:39:23 2014 +0200
7.3 @@ -25,7 +25,7 @@
7.4 def exit_error(exn: Throwable): Nothing =
7.5 {
7.6 GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
7.7 - system_dialog.return_code(2)
7.8 + system_dialog.return_code(Exn.return_code(exn, 2))
7.9 system_dialog.join_exit
7.10 }
7.11
7.12 @@ -60,7 +60,7 @@
7.13 build_heap = true, more_dirs = more_dirs,
7.14 system_mode = system_mode, sessions = List(session)))
7.15 }
7.16 - catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }
7.17 + catch { case exn: Throwable => (Exn.message(exn) + "\n", Exn.return_code(exn, 2)) }
7.18
7.19 system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
7.20 system_dialog.return_code(rc)
7.21 @@ -155,7 +155,7 @@
7.22 catch { case exn: Throwable => exit_error(exn) }
7.23
7.24 if (system_dialog.stopped) {
7.25 - system_dialog.return_code(130)
7.26 + system_dialog.return_code(Exn.Interrupt.return_code)
7.27 system_dialog.join_exit
7.28 }
7.29 }