more abstract Exn.Interrupt and POSIX return code;
authorwenzelm
Wed Apr 23 12:39:23 2014 +0200 (2014-04-23)
changeset 5666765e84b0ef974
parent 56666 229309cbc508
child 56668 56335a8e2e8b
more abstract Exn.Interrupt and POSIX return code;
src/Pure/Concurrent/simple_thread.scala
src/Pure/General/exn.ML
src/Pure/General/exn.scala
src/Pure/System/invoke_scala.scala
src/Pure/System/isabelle_system.scala
src/Pure/Tools/build.scala
src/Pure/Tools/main.scala
     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      }