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