src/Pure/System/bash.scala
author wenzelm
Sun, 21 Feb 2021 00:49:09 +0100
changeset 73265 76c9fcf80f96
parent 73263 ad60214bef09
child 73268 c8abfe393c16
permissions -rw-r--r--
clarified lines (again);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62584
6cd36a0d2a28 clarified files;
wenzelm
parents: 62574
diff changeset
     1
/*  Title:      Pure/System/bash.scala
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     3
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     4
GNU bash processes, with propagation of interrupts.
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     5
*/
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     6
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     7
package isabelle
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     8
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
     9
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    10
import java.io.{File => JFile, BufferedReader, InputStreamReader,
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    11
  BufferedWriter, OutputStreamWriter}
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    12
71706
wenzelm
parents: 71705
diff changeset
    13
import scala.annotation.tailrec
wenzelm
parents: 71705
diff changeset
    14
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    15
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    16
object Bash
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    17
{
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    18
  /* concrete syntax */
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    19
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    20
  private def bash_chr(c: Byte): String =
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    21
  {
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    22
    val ch = c.toChar
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    23
    ch match {
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    24
      case '\t' => "$'\\t'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    25
      case '\n' => "$'\\n'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    26
      case '\f' => "$'\\f'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    27
      case '\r' => "$'\\r'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    28
      case _ =>
67200
wenzelm
parents: 65317
diff changeset
    29
        if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+,-./:_".contains(ch))
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    30
          Symbol.ascii(ch)
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    31
        else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    32
        else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    33
        else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'"
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    34
        else  "\\" + ch
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    35
    }
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    36
  }
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    37
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    38
  def string(s: String): String =
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    39
    if (s == "") "\"\""
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 67200
diff changeset
    40
    else UTF8.bytes(s).iterator.map(bash_chr).mkString
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    41
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    42
  def strings(ss: List[String]): String =
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 67200
diff changeset
    43
    ss.iterator.map(Bash.string).mkString(" ")
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    44
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    45
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    46
  /* process and result */
96bc94c87a81 clarified modules;
wenzelm
parents: 63996
diff changeset
    47
72598
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
    48
  type Watchdog = (Time, Process => Boolean)
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
    49
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
    50
  def process(script: String,
62573
27f90319a499 isabelle.Build uses ML_Process directly;
wenzelm
parents: 62569
diff changeset
    51
      cwd: JFile = null,
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62604
diff changeset
    52
      env: Map[String, String] = Isabelle_System.settings(),
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    53
      redirect: Boolean = false,
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    54
      cleanup: () => Unit = () => ()): Process =
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    55
    new Process(script, cwd, env, redirect, cleanup)
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    56
63996
3f47fec9edfc tuned whitespace;
wenzelm
parents: 63805
diff changeset
    57
  class Process private[Bash](
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    58
      script: String,
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    59
      cwd: JFile,
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    60
      env: Map[String, String],
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    61
      redirect: Boolean,
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
    62
      cleanup: () => Unit)
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    63
  {
62604
wenzelm
parents: 62602
diff changeset
    64
    private val timing_file = Isabelle_System.tmp_file("bash_timing")
62569
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
    65
    private val timing = Synchronized[Option[Timing]](None)
65317
b9f5cd845616 more informative session result;
wenzelm
parents: 65316
diff changeset
    66
    def get_timing: Timing = timing.value getOrElse Timing.zero
62569
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
    67
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
    68
    private val script_file = Isabelle_System.tmp_file("bash_script")
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
    69
    File.write(script_file, script)
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
    70
62296
b04a5ddd6121 clarified bash process -- similar to ML version;
wenzelm
parents: 61025
diff changeset
    71
    private val proc =
62610
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62604
diff changeset
    72
      Isabelle_System.process(
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62604
diff changeset
    73
        List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62604
diff changeset
    74
          File.standard_path(timing_file), "bash", File.standard_path(script_file)),
4c89504c76fb more uniform signature for various process invocations;
wenzelm
parents: 62604
diff changeset
    75
        cwd = cwd, env = env, redirect = redirect)
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    76
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    77
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    78
    // channels
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    79
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    80
    val stdin: BufferedWriter =
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    81
      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    82
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    83
    val stdout: BufferedReader =
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    84
      new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    85
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    86
    val stderr: BufferedReader =
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    87
      new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    88
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    89
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    90
    // signals
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    91
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    92
    private val pid = stdout.readLine
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    93
71707
wenzelm
parents: 71706
diff changeset
    94
    @tailrec private def kill(signal: String, count: Int = 1): Boolean =
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
    95
    {
71706
wenzelm
parents: 71705
diff changeset
    96
      count <= 0 ||
wenzelm
parents: 71705
diff changeset
    97
      {
71707
wenzelm
parents: 71706
diff changeset
    98
        Isabelle_System.kill(signal, pid)
wenzelm
parents: 71706
diff changeset
    99
        val running = Isabelle_System.kill("0", pid)._2 == 0
wenzelm
parents: 71706
diff changeset
   100
        if (running) {
71705
7b75d52a1bf1 clarified interrupt handling;
wenzelm
parents: 71684
diff changeset
   101
          Time.seconds(0.1).sleep
71707
wenzelm
parents: 71706
diff changeset
   102
          kill(signal, count - 1)
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   103
        }
71706
wenzelm
parents: 71705
diff changeset
   104
        else false
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   105
      }
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   106
    }
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   107
71712
c6b7f4da67b3 more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents: 71708
diff changeset
   108
    def terminate(): Unit = Isabelle_Thread.try_uninterruptible
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   109
    {
71708
dd9fc8a3036c terminate faster;
wenzelm
parents: 71707
diff changeset
   110
      kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL")
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   111
      proc.destroy
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
   112
      do_cleanup()
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   113
    }
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   114
71712
c6b7f4da67b3 more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents: 71708
diff changeset
   115
    def interrupt(): Unit = Isabelle_Thread.try_uninterruptible
71705
7b75d52a1bf1 clarified interrupt handling;
wenzelm
parents: 71684
diff changeset
   116
    {
7b75d52a1bf1 clarified interrupt handling;
wenzelm
parents: 71684
diff changeset
   117
      Isabelle_System.kill("INT", pid)
7b75d52a1bf1 clarified interrupt handling;
wenzelm
parents: 71684
diff changeset
   118
    }
7b75d52a1bf1 clarified interrupt handling;
wenzelm
parents: 71684
diff changeset
   119
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   120
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   121
    // JVM shutdown hook
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   122
71712
c6b7f4da67b3 more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents: 71708
diff changeset
   123
    private val shutdown_hook = Isabelle_Thread.create(() => terminate())
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   124
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   125
    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   126
    catch { case _: IllegalStateException => }
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   127
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
   128
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   129
    // cleanup
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
   130
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
   131
    private def do_cleanup()
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
   132
    {
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   133
      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   134
      catch { case _: IllegalStateException => }
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   135
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
   136
      script_file.delete
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   137
62569
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
   138
      timing.change {
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
   139
        case None =>
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   140
          if (timing_file.isFile) {
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   141
            val t =
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   142
              Word.explode(File.read(timing_file)) match {
63805
c272680df665 clarified modules;
wenzelm
parents: 62610
diff changeset
   143
                case List(Value.Long(elapsed), Value.Long(cpu)) =>
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   144
                  Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   145
                case _ => Timing.zero
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   146
              }
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   147
            timing_file.delete
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   148
            Some(t)
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   149
          }
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   150
          else Some(Timing.zero)
62569
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
   151
        case some => some
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
   152
      }
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
   153
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
   154
      cleanup()
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   155
    }
62569
5db10482f4cf bash process with builtin timing;
wenzelm
parents: 62558
diff changeset
   156
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   157
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   158
    // join
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   159
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   160
    def join: Int =
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   161
    {
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   162
      val rc = proc.waitFor
62602
96e679f042ec more thorough cleanup -- in Scala;
wenzelm
parents: 62584
diff changeset
   163
      do_cleanup()
62545
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
   164
      rc
8ebffdaf2ce2 Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents: 62543
diff changeset
   165
    }
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   166
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   167
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   168
    // result
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   169
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   170
    def result(
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   171
      progress_stdout: String => Unit = (_: String) => (),
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   172
      progress_stderr: String => Unit = (_: String) => (),
72598
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   173
      watchdog: Option[Watchdog] = None,
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   174
      strict: Boolean = true): Process_Result =
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   175
    {
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   176
      stdin.close
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   177
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   178
      val out_lines =
72105
a1fb4d28e609 unused --- superseded by PIDE messages;
wenzelm
parents: 71712
diff changeset
   179
        Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) }
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   180
      val err_lines =
72105
a1fb4d28e609 unused --- superseded by PIDE messages;
wenzelm
parents: 71712
diff changeset
   181
        Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) }
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   182
72598
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   183
      val watchdog_thread =
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   184
        for ((time, check) <- watchdog)
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   185
        yield {
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   186
          Future.thread("bash_watchdog") {
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   187
            while (proc.isAlive) {
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   188
              time.sleep
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   189
              if (check(this)) interrupt()
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   190
            }
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   191
          }
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   192
        }
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   193
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   194
      val rc =
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   195
        try { join }
62574
ec382bc689e5 more robust cleanup;
wenzelm
parents: 62573
diff changeset
   196
        catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
72598
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   197
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   198
      watchdog_thread.foreach(_.cancel)
d9f2be66ebad support for watchdog thread;
wenzelm
parents: 72105
diff changeset
   199
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   200
      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   201
73134
8a8ffe78eee7 clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents: 72598
diff changeset
   202
      Process_Result(rc, out_lines.join, err_lines.join, get_timing)
62543
57f379ef662f clarified modules;
wenzelm
parents: 62400
diff changeset
   203
    }
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   204
  }
73228
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   205
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   206
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   207
  /* Scala function */
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   208
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   209
  object Process extends Scala.Fun("bash_process")
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   210
  {
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   211
    val here = Scala_Project.here
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   212
    def apply(script: String): String =
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   213
    {
73263
ad60214bef09 more uniform Bash.process: always ask Isabelle/Scala;
wenzelm
parents: 73230
diff changeset
   214
      val result = Exn.capture { Isabelle_System.bash(script) }
73228
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   215
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   216
      val is_interrupt =
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   217
        result match {
73263
ad60214bef09 more uniform Bash.process: always ask Isabelle/Scala;
wenzelm
parents: 73230
diff changeset
   218
          case Exn.Res(res) => res.rc == Exn.Interrupt.return_code
73228
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   219
          case Exn.Exn(exn) => Exn.is_interrupt(exn)
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   220
        }
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   221
73263
ad60214bef09 more uniform Bash.process: always ask Isabelle/Scala;
wenzelm
parents: 73230
diff changeset
   222
      val encode: XML.Encode.T[Exn.Result[Process_Result]] =
73228
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   223
      {
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   224
        import XML.Encode._
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   225
        val string = XML.Encode.string
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   226
        variant(List(
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   227
          { case _ if is_interrupt => (Nil, Nil) },
73230
d1bc5a376cf9 more robust: allow YXML text;
wenzelm
parents: 73228
diff changeset
   228
          { case Exn.Exn(exn) => (Nil, string(Exn.message(exn))) },
73263
ad60214bef09 more uniform Bash.process: always ask Isabelle/Scala;
wenzelm
parents: 73230
diff changeset
   229
          { case Exn.Res(res) =>
73265
76c9fcf80f96 clarified lines (again);
wenzelm
parents: 73263
diff changeset
   230
              val out = if (res.out_lines.isEmpty) "" else Library.terminate_lines(res.out_lines)
76c9fcf80f96 clarified lines (again);
wenzelm
parents: 73263
diff changeset
   231
              val err = if (res.err_lines.isEmpty) "" else Library.terminate_lines(res.err_lines)
73263
ad60214bef09 more uniform Bash.process: always ask Isabelle/Scala;
wenzelm
parents: 73230
diff changeset
   232
              (List(int_atom(res.rc)), pair(string, string)(out, err)) }))
73228
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   233
      }
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   234
      YXML.string_of_body(encode(result))
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   235
    }
0575cfd2ecfc support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents: 73134
diff changeset
   236
  }
60991
2fc5a44346b5 clarified modules, like ML version;
wenzelm
parents:
diff changeset
   237
}