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