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