src/Pure/Tools/isabelle_process.scala
author wenzelm
Sun Aug 24 21:15:46 2008 +0200 (2008-08-24 ago)
changeset 27990 f9dd4c9ed812
parent 27973 18d02c0b90b6
child 27992 131f7ea9e6e6
permissions -rw-r--r--
Kind: added is_control;
more robust kill/exit;
tuned interfaces;
wenzelm@27963
     1
/*  Title:      Pure/Tools/isabelle_process.ML
wenzelm@27949
     2
    ID:         $Id$
wenzelm@27949
     3
    Author:     Makarius
wenzelm@27963
     4
    Options:    :folding=explicit:collapseFolds=1:
wenzelm@27949
     5
wenzelm@27949
     6
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm@27949
     7
*/
wenzelm@27949
     8
wenzelm@27949
     9
package isabelle
wenzelm@27949
    10
wenzelm@27949
    11
import java.util.Properties
wenzelm@27955
    12
import java.util.concurrent.LinkedBlockingQueue
wenzelm@27949
    13
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, IOException}
wenzelm@27949
    14
wenzelm@27963
    15
import isabelle.{Symbol, XML}
wenzelm@27949
    16
wenzelm@27949
    17
wenzelm@27973
    18
object IsabelleProcess {
wenzelm@27973
    19
wenzelm@27973
    20
  /* exception */
wenzelm@27949
    21
wenzelm@27955
    22
  class IsabelleProcessException(msg: String) extends Exception {
wenzelm@27955
    23
    override def toString = "IsabelleProcess: " + msg
wenzelm@27955
    24
  }
wenzelm@27949
    25
wenzelm@27949
    26
wenzelm@27949
    27
  /* results */
wenzelm@27949
    28
wenzelm@27949
    29
  object Kind extends Enumeration {
wenzelm@27949
    30
    //{{{ values
wenzelm@27949
    31
    // Posix channels/events
wenzelm@27949
    32
    val STDIN = Value("STDIN")
wenzelm@27949
    33
    val STDOUT = Value("STDOUT")
wenzelm@27949
    34
    val STDERR = Value("STDERR")
wenzelm@27949
    35
    val SIGNAL = Value("SIGNAL")
wenzelm@27949
    36
    val EXIT = Value("EXIT")
wenzelm@27949
    37
    // Isabelle messages
wenzelm@27949
    38
    val WRITELN = Value("WRITELN")
wenzelm@27949
    39
    val PRIORITY = Value("PRIORITY")
wenzelm@27949
    40
    val TRACING = Value("TRACING")
wenzelm@27949
    41
    val WARNING = Value("WARNING")
wenzelm@27949
    42
    val ERROR = Value("ERROR")
wenzelm@27949
    43
    val DEBUG = Value("DEBUG")
wenzelm@27949
    44
    val PROMPT = Value("PROMPT")
wenzelm@27949
    45
    val INIT = Value("INIT")
wenzelm@27949
    46
    val STATUS = Value("STATUS")
wenzelm@27949
    47
    // internal system notification
wenzelm@27949
    48
    val SYSTEM = Value("SYSTEM")
wenzelm@27949
    49
    //}}}
wenzelm@27949
    50
    def is_raw(kind: Value) =
wenzelm@27949
    51
      kind == STDOUT ||
wenzelm@27949
    52
      kind == STDERR
wenzelm@27990
    53
    def is_control(kind: Value) =
wenzelm@27990
    54
      kind == SIGNAL ||
wenzelm@27990
    55
      kind == EXIT ||
wenzelm@27990
    56
      kind == SYSTEM
wenzelm@27949
    57
    def is_system(kind: Value) =
wenzelm@27949
    58
      kind == STDIN ||
wenzelm@27949
    59
      kind == SIGNAL ||
wenzelm@27949
    60
      kind == EXIT ||
wenzelm@27949
    61
      kind == PROMPT ||
wenzelm@27949
    62
      kind == STATUS ||
wenzelm@27949
    63
      kind == SYSTEM
wenzelm@27949
    64
  }
wenzelm@27949
    65
wenzelm@27973
    66
  class Result(val kind: Kind.Value, val props: Properties, val result: String) {
wenzelm@27949
    67
    override def toString = {
wenzelm@27963
    68
      val res = XML.content(YXML.parse_failsafe(result)).mkString("")
wenzelm@27955
    69
      if (props == null) kind.toString + " [[" + res + "]]"
wenzelm@27955
    70
      else kind.toString + " " + props.toString + " [[" + res + "]]"
wenzelm@27949
    71
    }
wenzelm@27973
    72
    def is_raw() = Kind.is_raw(kind)
wenzelm@27990
    73
    def is_control() = Kind.is_control(kind)
wenzelm@27973
    74
    def is_system() = Kind.is_system(kind)
wenzelm@27973
    75
  }
wenzelm@27949
    76
wenzelm@27973
    77
}
wenzelm@27973
    78
wenzelm@27973
    79
wenzelm@27973
    80
class IsabelleProcess(args: String*) {
wenzelm@27973
    81
wenzelm@27973
    82
  import IsabelleProcess._
wenzelm@27973
    83
wenzelm@27973
    84
wenzelm@27973
    85
  /* process information */
wenzelm@27973
    86
wenzelm@27973
    87
  private var proc: Process = null
wenzelm@27973
    88
  private var closing = false
wenzelm@27973
    89
  private var pid: String = null
wenzelm@27973
    90
  private var the_session: String = null
wenzelm@27973
    91
  def session() = the_session
wenzelm@27973
    92
wenzelm@27973
    93
wenzelm@27990
    94
  /* symbols */
wenzelm@27990
    95
wenzelm@27990
    96
  val symbols = new Symbol.Interpretation
wenzelm@27990
    97
  def decode_result(result: Result) = YXML.parse_failsafe(symbols.decode(result.result))
wenzelm@27990
    98
wenzelm@27990
    99
wenzelm@27973
   100
  /* results */
wenzelm@27949
   101
wenzelm@27990
   102
  private val results = new LinkedBlockingQueue[Result]
wenzelm@27949
   103
wenzelm@27949
   104
  private def put_result(kind: Kind.Value, props: Properties, result: String) {
wenzelm@27963
   105
    if (kind == Kind.INIT && props != null) {
wenzelm@27973
   106
      pid = props.getProperty(Markup.PID)
wenzelm@27973
   107
      the_session = props.getProperty(Markup.SESSION)
wenzelm@27963
   108
    }
wenzelm@27955
   109
    results.put(new Result(kind, props, result))
wenzelm@27949
   110
  }
wenzelm@27949
   111
wenzelm@27990
   112
  def get_result() = results.take
wenzelm@27973
   113
wenzelm@27973
   114
wenzelm@27973
   115
  /* signals */
wenzelm@27973
   116
wenzelm@27973
   117
  def interrupt() = synchronized {
wenzelm@27973
   118
    if (proc == null) throw new IsabelleProcessException("Cannot interrupt: no process")
wenzelm@27973
   119
    if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
wenzelm@27973
   120
    else {
wenzelm@27973
   121
      try {
wenzelm@27990
   122
        if (IsabelleSystem.exec(List("kill", "-INT", pid)).waitFor == 0)
wenzelm@27990
   123
          put_result(Kind.SIGNAL, null, "INT")
wenzelm@27990
   124
        else
wenzelm@27973
   125
          put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
wenzelm@27973
   126
      }
wenzelm@27973
   127
      catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) }
wenzelm@27973
   128
    }
wenzelm@27973
   129
  }
wenzelm@27973
   130
wenzelm@27973
   131
  def kill() = synchronized {
wenzelm@27973
   132
    if (proc == 0) throw new IsabelleProcessException("Cannot kill: no process")
wenzelm@27973
   133
    else {
wenzelm@27973
   134
      try_close()
wenzelm@27990
   135
      Thread.sleep(500)
wenzelm@27973
   136
      put_result(Kind.SIGNAL, null, "KILL")
wenzelm@27973
   137
      proc.destroy
wenzelm@27973
   138
      proc = null
wenzelm@27990
   139
      pid = null
wenzelm@27973
   140
    }
wenzelm@27973
   141
  }
wenzelm@27973
   142
wenzelm@27949
   143
wenzelm@27949
   144
  /* output being piped into the process */
wenzelm@27949
   145
wenzelm@27990
   146
  private val output = new LinkedBlockingQueue[String]
wenzelm@27949
   147
wenzelm@27949
   148
  def output_raw(text: String) = synchronized {
wenzelm@27949
   149
    if (proc == null) throw new IsabelleProcessException("Cannot output: no process")
wenzelm@27949
   150
    if (closing) throw new IsabelleProcessException("Cannot output: already closing")
wenzelm@27955
   151
    output.put(text)
wenzelm@27949
   152
  }
wenzelm@27949
   153
wenzelm@27949
   154
  def output_sync(text: String) = output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
wenzelm@27949
   155
wenzelm@27963
   156
wenzelm@27963
   157
  def command(text: String) =
wenzelm@27949
   158
    output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text))
wenzelm@27949
   159
wenzelm@27963
   160
  def command(props: Properties, text: String) =
wenzelm@27949
   161
    output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " +
wenzelm@27949
   162
      IsabelleSyntax.encode_string(text))
wenzelm@27949
   163
wenzelm@27963
   164
  def ML(text: String) =
wenzelm@27949
   165
    output_sync("ML_val " + IsabelleSyntax.encode_string(text))
wenzelm@27949
   166
wenzelm@27949
   167
  def close() = synchronized {    // FIXME watchdog/timeout
wenzelm@27949
   168
    output_raw("\u0000")
wenzelm@27949
   169
    closing = true
wenzelm@27949
   170
  }
wenzelm@27949
   171
wenzelm@27949
   172
  def try_close() = synchronized {
wenzelm@27949
   173
    if (proc != null && !closing) {
wenzelm@27949
   174
      try { close() }
wenzelm@27949
   175
      catch { case _: IsabelleProcessException => () }
wenzelm@27949
   176
    }
wenzelm@27949
   177
  }
wenzelm@27949
   178
wenzelm@27949
   179
wenzelm@27949
   180
  /* stdin */
wenzelm@27949
   181
wenzelm@27949
   182
  private class StdinThread(writer: BufferedWriter) extends Thread {
wenzelm@27949
   183
    override def run() = {
wenzelm@27949
   184
      var finished = false
wenzelm@27949
   185
      while (!finished) {
wenzelm@27949
   186
        try {
wenzelm@27949
   187
          //{{{
wenzelm@27955
   188
          val s = output.take
wenzelm@27949
   189
          if (s == "\u0000") {
wenzelm@27949
   190
            writer.close
wenzelm@27949
   191
            finished = true
wenzelm@27949
   192
          }
wenzelm@27949
   193
          else {
wenzelm@27949
   194
            put_result(Kind.STDIN, null, s)
wenzelm@27949
   195
            writer.write(s)
wenzelm@27949
   196
            writer.flush
wenzelm@27949
   197
          }
wenzelm@27949
   198
          //}}}
wenzelm@27949
   199
        }
wenzelm@27949
   200
        catch {
wenzelm@27949
   201
          case e: IOException => put_result(Kind.SYSTEM, null, "Stdin thread: " + e.getMessage)
wenzelm@27949
   202
        }
wenzelm@27949
   203
      }
wenzelm@27949
   204
      put_result(Kind.SYSTEM, null, "Stdin thread terminated")
wenzelm@27949
   205
    }
wenzelm@27949
   206
  }
wenzelm@27949
   207
wenzelm@27949
   208
wenzelm@27949
   209
  /* stdout */
wenzelm@27949
   210
wenzelm@27949
   211
  private class StdoutThread(reader: BufferedReader) extends Thread {
wenzelm@27949
   212
    override def run() = {
wenzelm@27949
   213
      var kind = Kind.STDOUT
wenzelm@27949
   214
      var props: Properties = null
wenzelm@27949
   215
      var result = new StringBuilder
wenzelm@27949
   216
wenzelm@27949
   217
      var finished = false
wenzelm@27949
   218
      while (!finished) {
wenzelm@27949
   219
        try {
wenzelm@27949
   220
          if (kind == Kind.STDOUT) {
wenzelm@27949
   221
            //{{{ Char mode
wenzelm@27949
   222
            var c = -1
wenzelm@27949
   223
            var done = false
wenzelm@27949
   224
            while (!done && (result.length == 0 || reader.ready)) {
wenzelm@27949
   225
              c = reader.read
wenzelm@27949
   226
              if (c > 0 && c != 2) result.append(c.asInstanceOf[Char])
wenzelm@27949
   227
              else done = true
wenzelm@27949
   228
            }
wenzelm@27949
   229
            if (result.length > 0) {
wenzelm@27949
   230
              put_result(kind, null, result.toString)
wenzelm@27949
   231
              result.length = 0
wenzelm@27949
   232
            }
wenzelm@27949
   233
            if (c == -1) {
wenzelm@27949
   234
              reader.close
wenzelm@27949
   235
              finished = true
wenzelm@27949
   236
              try_close()
wenzelm@27949
   237
            }
wenzelm@27949
   238
            else if (c == 2) {
wenzelm@27949
   239
              reader.read match {
wenzelm@27949
   240
                case 'A' => kind = Kind.WRITELN
wenzelm@27949
   241
                case 'B' => kind = Kind.PRIORITY
wenzelm@27949
   242
                case 'C' => kind = Kind.TRACING
wenzelm@27949
   243
                case 'D' => kind = Kind.WARNING
wenzelm@27949
   244
                case 'E' => kind = Kind.ERROR
wenzelm@27949
   245
                case 'F' => kind = Kind.DEBUG
wenzelm@27949
   246
                case 'G' => kind = Kind.PROMPT
wenzelm@27949
   247
                case 'H' => kind = Kind.INIT
wenzelm@27949
   248
                case 'I' => kind = Kind.STATUS
wenzelm@27949
   249
                case _ => kind = Kind.STDOUT
wenzelm@27949
   250
              }
wenzelm@27949
   251
              props = null
wenzelm@27949
   252
            }
wenzelm@27949
   253
            //}}}
wenzelm@27949
   254
          }
wenzelm@27949
   255
          else {
wenzelm@27949
   256
            //{{{ Line mode
wenzelm@27949
   257
            val line = reader.readLine
wenzelm@27949
   258
            if (line == null) {
wenzelm@27949
   259
              reader.close
wenzelm@27949
   260
              finished = true
wenzelm@27949
   261
              try_close()
wenzelm@27949
   262
            }
wenzelm@27949
   263
            else {
wenzelm@27949
   264
              val len = line.length
wenzelm@27949
   265
              // property
wenzelm@27949
   266
              if (line.endsWith("\u0002,")) {
wenzelm@27949
   267
                val i = line.indexOf('=')
wenzelm@27949
   268
                if (i > 0) {
wenzelm@27949
   269
                  val name = line.substring(0, i)
wenzelm@27949
   270
                  val value = line.substring(i + 1, len - 2)
wenzelm@27949
   271
                  if (props == null) props = new Properties
wenzelm@27963
   272
                  if (!props.containsKey(name)) props.setProperty(name, value)
wenzelm@27949
   273
                }
wenzelm@27949
   274
              }
wenzelm@27949
   275
              // last text line
wenzelm@27949
   276
              else if (line.endsWith("\u0002.")) {
wenzelm@27949
   277
                result.append(line.substring(0, len - 2))
wenzelm@27949
   278
                put_result(kind, props, result.toString)
wenzelm@27949
   279
                result.length = 0
wenzelm@27949
   280
                kind = Kind.STDOUT
wenzelm@27949
   281
              }
wenzelm@27949
   282
              // text line
wenzelm@27949
   283
              else {
wenzelm@27949
   284
                result.append(line)
wenzelm@27949
   285
                result.append('\n')
wenzelm@27949
   286
              }
wenzelm@27949
   287
            }
wenzelm@27949
   288
            //}}}
wenzelm@27949
   289
          }
wenzelm@27963
   290
        }
wenzelm@27963
   291
        catch {
wenzelm@27949
   292
          case e: IOException => put_result(Kind.SYSTEM, null, "Stdout thread: " + e.getMessage)
wenzelm@27949
   293
        }
wenzelm@27949
   294
      }
wenzelm@27949
   295
      put_result(Kind.SYSTEM, null, "Stdout thread terminated")
wenzelm@27949
   296
    }
wenzelm@27949
   297
  }
wenzelm@27949
   298
wenzelm@27949
   299
wenzelm@27949
   300
  /* stderr */
wenzelm@27949
   301
wenzelm@27949
   302
  private class StderrThread(reader: BufferedReader) extends Thread {
wenzelm@27949
   303
    override def run() = {
wenzelm@27949
   304
      var result = new StringBuilder(100)
wenzelm@27949
   305
wenzelm@27949
   306
      var finished = false
wenzelm@27949
   307
      while (!finished) {
wenzelm@27949
   308
        try {
wenzelm@27949
   309
          //{{{
wenzelm@27949
   310
          var c = -1
wenzelm@27949
   311
          var done = false
wenzelm@27949
   312
          while (!done && (result.length == 0 || reader.ready)) {
wenzelm@27949
   313
            c = reader.read
wenzelm@27949
   314
            if (c > 0) result.append(c.asInstanceOf[Char])
wenzelm@27949
   315
            else done = true
wenzelm@27949
   316
          }
wenzelm@27949
   317
          if (result.length > 0) {
wenzelm@27949
   318
            put_result(Kind.STDERR, null, result.toString)
wenzelm@27949
   319
            result.length = 0
wenzelm@27949
   320
          }
wenzelm@27949
   321
          else {
wenzelm@27949
   322
            reader.close
wenzelm@27949
   323
            finished = true
wenzelm@27949
   324
            try_close()
wenzelm@27949
   325
          }
wenzelm@27949
   326
          //}}}
wenzelm@27963
   327
        }
wenzelm@27963
   328
        catch {
wenzelm@27949
   329
          case e: IOException => put_result(Kind.SYSTEM, null, "Stderr thread: " + e.getMessage)
wenzelm@27949
   330
        }
wenzelm@27949
   331
      }
wenzelm@27949
   332
      put_result(Kind.SYSTEM, null, "Stderr thread terminated")
wenzelm@27949
   333
    }
wenzelm@27949
   334
  }
wenzelm@27949
   335
wenzelm@27949
   336
wenzelm@27949
   337
  /* exit */
wenzelm@27949
   338
wenzelm@27949
   339
  private class ExitThread extends Thread {
wenzelm@27949
   340
    override def run() = {
wenzelm@27990
   341
      val rc = proc.waitFor()
wenzelm@27949
   342
      Thread.sleep(300)
wenzelm@27949
   343
      put_result(Kind.SYSTEM, null, "Exit thread terminated")
wenzelm@27949
   344
      put_result(Kind.EXIT, null, Integer.toString(rc))
wenzelm@27949
   345
    }
wenzelm@27949
   346
  }
wenzelm@27949
   347
wenzelm@27949
   348
wenzelm@27949
   349
wenzelm@27949
   350
  /** main **/
wenzelm@27949
   351
wenzelm@27949
   352
  {
wenzelm@27973
   353
    /* exec process */
wenzelm@27963
   354
wenzelm@27973
   355
    try {
wenzelm@27973
   356
      proc = IsabelleSystem.exec(List(
wenzelm@27973
   357
        IsabelleSystem.getenv_strict("ISABELLE_HOME") + "/bin/isabelle-process", "-W") ++ args)
wenzelm@27949
   358
    }
wenzelm@27973
   359
    catch { case e: IOException => throw new IsabelleProcessException(e.getMessage) }
wenzelm@27949
   360
wenzelm@27949
   361
wenzelm@27973
   362
    /* control process via threads */
wenzelm@27949
   363
wenzelm@27973
   364
    val charset = "UTF-8"
wenzelm@27949
   365
    new StdinThread(new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, charset))).start
wenzelm@27949
   366
    new StdoutThread(new BufferedReader(new InputStreamReader(proc.getInputStream, charset))).start
wenzelm@27949
   367
    new StderrThread(new BufferedReader(new InputStreamReader(proc.getErrorStream, charset))).start
wenzelm@27949
   368
    new ExitThread().start
wenzelm@27949
   369
  }
wenzelm@27949
   370
wenzelm@27949
   371
}