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