src/Pure/Tools/isabelle_process.scala
author wenzelm
Mon Dec 29 15:23:56 2008 +0100 (2008-12-29 ago)
changeset 29194 53930d089f88
parent 29192 082ee2a01a6d
child 29196 de62fdd4b432
permissions -rw-r--r--
tuned;
wenzelm@27963
     1
/*  Title:      Pure/Tools/isabelle_process.ML
wenzelm@27949
     2
    Author:     Makarius
wenzelm@27963
     3
    Options:    :folding=explicit:collapseFolds=1:
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@28045
    12
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
wenzelm@28056
    13
  InputStream, OutputStream, IOException}
wenzelm@27949
    14
wenzelm@27949
    15
wenzelm@27973
    16
object IsabelleProcess {
wenzelm@27973
    17
wenzelm@27949
    18
  /* results */
wenzelm@27949
    19
wenzelm@27949
    20
  object Kind extends Enumeration {
wenzelm@28344
    21
    //{{{ values and codes
wenzelm@28344
    22
    // internal system notification
wenzelm@28344
    23
    val SYSTEM = Value("SYSTEM")
wenzelm@27949
    24
    // Posix channels/events
wenzelm@27949
    25
    val STDIN = Value("STDIN")
wenzelm@27949
    26
    val STDOUT = Value("STDOUT")
wenzelm@27949
    27
    val SIGNAL = Value("SIGNAL")
wenzelm@27949
    28
    val EXIT = Value("EXIT")
wenzelm@27949
    29
    // Isabelle messages
wenzelm@28344
    30
    val INIT = Value("INIT")
wenzelm@28344
    31
    val STATUS = Value("STATUS")
wenzelm@27949
    32
    val WRITELN = Value("WRITELN")
wenzelm@27949
    33
    val PRIORITY = Value("PRIORITY")
wenzelm@27949
    34
    val TRACING = Value("TRACING")
wenzelm@27949
    35
    val WARNING = Value("WARNING")
wenzelm@27949
    36
    val ERROR = Value("ERROR")
wenzelm@27949
    37
    val DEBUG = Value("DEBUG")
wenzelm@28344
    38
    // messages codes
wenzelm@28344
    39
    val code = Map(
wenzelm@28344
    40
      ('A' : Int) -> Kind.INIT,
wenzelm@28344
    41
      ('B' : Int) -> Kind.STATUS,
wenzelm@28344
    42
      ('C' : Int) -> Kind.WRITELN,
wenzelm@28344
    43
      ('D' : Int) -> Kind.PRIORITY,
wenzelm@28344
    44
      ('E' : Int) -> Kind.TRACING,
wenzelm@28344
    45
      ('F' : Int) -> Kind.WARNING,
wenzelm@28344
    46
      ('G' : Int) -> Kind.ERROR,
wenzelm@28344
    47
      ('H' : Int) -> Kind.DEBUG,
wenzelm@28344
    48
      ('0' : Int) -> Kind.SYSTEM,
wenzelm@28344
    49
      ('1' : Int) -> Kind.STDIN,
wenzelm@28344
    50
      ('2' : Int) -> Kind.STDOUT,
wenzelm@28344
    51
      ('3' : Int) -> Kind.SIGNAL,
wenzelm@28344
    52
      ('4' : Int) -> Kind.EXIT)
wenzelm@27949
    53
    //}}}
wenzelm@27949
    54
    def is_raw(kind: Value) =
wenzelm@28045
    55
      kind == STDOUT
wenzelm@27990
    56
    def is_control(kind: Value) =
wenzelm@28344
    57
      kind == SYSTEM ||
wenzelm@27990
    58
      kind == SIGNAL ||
wenzelm@28344
    59
      kind == EXIT
wenzelm@27949
    60
    def is_system(kind: Value) =
wenzelm@28344
    61
      kind == SYSTEM ||
wenzelm@27949
    62
      kind == STDIN ||
wenzelm@27949
    63
      kind == SIGNAL ||
wenzelm@27949
    64
      kind == EXIT ||
wenzelm@28498
    65
      kind == STATUS
wenzelm@27949
    66
  }
wenzelm@27949
    67
wenzelm@27973
    68
  class Result(val kind: Kind.Value, val props: Properties, val result: String) {
wenzelm@27949
    69
    override def toString = {
wenzelm@29174
    70
      val res = XML.content(YXML.parse_failsafe(result)).mkString
wenzelm@27955
    71
      if (props == null) kind.toString + " [[" + res + "]]"
wenzelm@27955
    72
      else kind.toString + " " + props.toString + " [[" + res + "]]"
wenzelm@27949
    73
    }
wenzelm@29192
    74
    def is_raw = Kind.is_raw(kind)
wenzelm@29192
    75
    def is_control = Kind.is_control(kind)
wenzelm@29192
    76
    def is_system = Kind.is_system(kind)
wenzelm@27973
    77
  }
wenzelm@27949
    78
wenzelm@27973
    79
}
wenzelm@27973
    80
wenzelm@27973
    81
wenzelm@29192
    82
class IsabelleProcess(isabelle_system: IsabelleSystem,
wenzelm@29192
    83
  results: EventBus[IsabelleProcess.Result], args: String*)
wenzelm@29192
    84
{
wenzelm@27973
    85
  import IsabelleProcess._
wenzelm@29194
    86
wenzelm@27973
    87
wenzelm@29192
    88
  /* demo constructor */
wenzelm@27973
    89
wenzelm@29192
    90
  def this(args: String*) =
wenzelm@29192
    91
    this(new IsabelleSystem, new EventBus[IsabelleProcess.Result] + (Console.println(_)), args: _*)
wenzelm@29174
    92
wenzelm@29174
    93
wenzelm@27973
    94
  /* process information */
wenzelm@27973
    95
wenzelm@27973
    96
  private var proc: Process = null
wenzelm@27973
    97
  private var closing = false
wenzelm@27973
    98
  private var pid: String = null
wenzelm@27973
    99
  private var the_session: String = null
wenzelm@27973
   100
  def session() = the_session
wenzelm@27973
   101
wenzelm@27973
   102
wenzelm@27973
   103
  /* results */
wenzelm@27949
   104
wenzelm@29192
   105
  private val result_queue = new LinkedBlockingQueue[Result]
wenzelm@27949
   106
wenzelm@27949
   107
  private def put_result(kind: Kind.Value, props: Properties, result: String) {
wenzelm@27963
   108
    if (kind == Kind.INIT && props != null) {
wenzelm@27973
   109
      pid = props.getProperty(Markup.PID)
wenzelm@27973
   110
      the_session = props.getProperty(Markup.SESSION)
wenzelm@27963
   111
    }
wenzelm@29192
   112
    result_queue.put(new Result(kind, props, result))
wenzelm@27949
   113
  }
wenzelm@27949
   114
wenzelm@29192
   115
  private class ResultThread extends Thread("isabelle: results") {
wenzelm@29192
   116
    override def run() = {
wenzelm@29192
   117
      var finished = false
wenzelm@29192
   118
      while (!finished) {
wenzelm@29192
   119
        val result =
wenzelm@29192
   120
          try { result_queue.take }
wenzelm@29192
   121
          catch { case _: NullPointerException => null }
wenzelm@27973
   122
wenzelm@29192
   123
        if (result != null) {
wenzelm@29192
   124
          results.event(result)  // FIXME try/catch (!??)
wenzelm@29192
   125
          if (result.kind == Kind.EXIT) finished = true
wenzelm@29192
   126
        }
wenzelm@29192
   127
        else finished = true
wenzelm@29192
   128
      }
wenzelm@29192
   129
    }
wenzelm@27992
   130
  }
wenzelm@27992
   131
wenzelm@27973
   132
wenzelm@27973
   133
  /* signals */
wenzelm@27973
   134
wenzelm@27973
   135
  def interrupt() = synchronized {
wenzelm@27993
   136
    if (proc == null) error("Cannot interrupt Isabelle: no process")
wenzelm@27973
   137
    if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid")
wenzelm@27973
   138
    else {
wenzelm@27973
   139
      try {
wenzelm@29178
   140
        if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0)
wenzelm@27990
   141
          put_result(Kind.SIGNAL, null, "INT")
wenzelm@27990
   142
        else
wenzelm@27973
   143
          put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed")
wenzelm@27973
   144
      }
wenzelm@27993
   145
      catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
wenzelm@27973
   146
    }
wenzelm@27973
   147
  }
wenzelm@27973
   148
wenzelm@27973
   149
  def kill() = synchronized {
wenzelm@27993
   150
    if (proc == 0) error("Cannot kill Isabelle: no process")
wenzelm@27973
   151
    else {
wenzelm@27973
   152
      try_close()
wenzelm@27990
   153
      Thread.sleep(500)
wenzelm@27973
   154
      put_result(Kind.SIGNAL, null, "KILL")
wenzelm@27973
   155
      proc.destroy
wenzelm@27973
   156
      proc = null
wenzelm@27990
   157
      pid = null
wenzelm@27973
   158
    }
wenzelm@27973
   159
  }
wenzelm@27973
   160
wenzelm@27949
   161
wenzelm@27949
   162
  /* output being piped into the process */
wenzelm@27949
   163
wenzelm@27990
   164
  private val output = new LinkedBlockingQueue[String]
wenzelm@27949
   165
wenzelm@28045
   166
  private def output_raw(text: String) = synchronized {
wenzelm@27993
   167
    if (proc == null) error("Cannot output to Isabelle: no process")
wenzelm@27993
   168
    if (closing) error("Cannot output to Isabelle: already closing")
wenzelm@27955
   169
    output.put(text)
wenzelm@27949
   170
  }
wenzelm@27949
   171
wenzelm@28303
   172
  def output_sync(text: String) =
wenzelm@28045
   173
    output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
wenzelm@27949
   174
wenzelm@27963
   175
wenzelm@27963
   176
  def command(text: String) =
wenzelm@27949
   177
    output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text))
wenzelm@27949
   178
wenzelm@27963
   179
  def command(props: Properties, text: String) =
wenzelm@27949
   180
    output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " +
wenzelm@27949
   181
      IsabelleSyntax.encode_string(text))
wenzelm@27949
   182
wenzelm@27963
   183
  def ML(text: String) =
wenzelm@27949
   184
    output_sync("ML_val " + IsabelleSyntax.encode_string(text))
wenzelm@27949
   185
wenzelm@27949
   186
  def close() = synchronized {    // FIXME watchdog/timeout
wenzelm@27949
   187
    output_raw("\u0000")
wenzelm@27949
   188
    closing = true
wenzelm@27949
   189
  }
wenzelm@27949
   190
wenzelm@27949
   191
  def try_close() = synchronized {
wenzelm@27949
   192
    if (proc != null && !closing) {
wenzelm@27949
   193
      try { close() }
wenzelm@27993
   194
      catch { case _: RuntimeException => }
wenzelm@27949
   195
    }
wenzelm@27949
   196
  }
wenzelm@27949
   197
wenzelm@27949
   198
wenzelm@27949
   199
  /* stdin */
wenzelm@27949
   200
wenzelm@28045
   201
  private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
wenzelm@27949
   202
    override def run() = {
wenzelm@29174
   203
      val writer = new BufferedWriter(new OutputStreamWriter(out_stream, isabelle_system.charset))
wenzelm@27949
   204
      var finished = false
wenzelm@27949
   205
      while (!finished) {
wenzelm@27949
   206
        try {
wenzelm@27949
   207
          //{{{
wenzelm@27955
   208
          val s = output.take
wenzelm@27949
   209
          if (s == "\u0000") {
wenzelm@27949
   210
            writer.close
wenzelm@27949
   211
            finished = true
wenzelm@27949
   212
          }
wenzelm@27949
   213
          else {
wenzelm@27949
   214
            put_result(Kind.STDIN, null, s)
wenzelm@27949
   215
            writer.write(s)
wenzelm@27949
   216
            writer.flush
wenzelm@27949
   217
          }
wenzelm@27949
   218
          //}}}
wenzelm@27949
   219
        }
wenzelm@27949
   220
        catch {
wenzelm@27949
   221
          case e: IOException => put_result(Kind.SYSTEM, null, "Stdin thread: " + e.getMessage)
wenzelm@27949
   222
        }
wenzelm@27949
   223
      }
wenzelm@27949
   224
      put_result(Kind.SYSTEM, null, "Stdin thread terminated")
wenzelm@27949
   225
    }
wenzelm@27949
   226
  }
wenzelm@27949
   227
wenzelm@27949
   228
wenzelm@27949
   229
  /* stdout */
wenzelm@27949
   230
wenzelm@28045
   231
  private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
wenzelm@27949
   232
    override def run() = {
wenzelm@29174
   233
      val reader = new BufferedReader(new InputStreamReader(in_stream, isabelle_system.charset))
wenzelm@28045
   234
      var result = new StringBuilder(100)
wenzelm@27949
   235
wenzelm@27949
   236
      var finished = false
wenzelm@27949
   237
      while (!finished) {
wenzelm@27949
   238
        try {
wenzelm@28045
   239
          //{{{
wenzelm@28045
   240
          var c = -1
wenzelm@28045
   241
          var done = false
wenzelm@28045
   242
          while (!done && (result.length == 0 || reader.ready)) {
wenzelm@28045
   243
            c = reader.read
wenzelm@28045
   244
            if (c >= 0) result.append(c.asInstanceOf[Char])
wenzelm@28045
   245
            else done = true
wenzelm@28045
   246
          }
wenzelm@28045
   247
          if (result.length > 0) {
wenzelm@28045
   248
            put_result(Kind.STDOUT, null, result.toString)
wenzelm@28045
   249
            result.length = 0
wenzelm@27949
   250
          }
wenzelm@27949
   251
          else {
wenzelm@28045
   252
            reader.close
wenzelm@28045
   253
            finished = true
wenzelm@28045
   254
            try_close()
wenzelm@27949
   255
          }
wenzelm@28045
   256
          //}}}
wenzelm@27963
   257
        }
wenzelm@27963
   258
        catch {
wenzelm@27949
   259
          case e: IOException => put_result(Kind.SYSTEM, null, "Stdout thread: " + e.getMessage)
wenzelm@27949
   260
        }
wenzelm@27949
   261
      }
wenzelm@27949
   262
      put_result(Kind.SYSTEM, null, "Stdout thread terminated")
wenzelm@27949
   263
    }
wenzelm@27949
   264
  }
wenzelm@27949
   265
wenzelm@27949
   266
wenzelm@28045
   267
  /* messages */
wenzelm@27949
   268
wenzelm@28045
   269
  private class MessageThread(fifo: String) extends Thread("isabelle: messages") {
wenzelm@27949
   270
    override def run() = {
wenzelm@29174
   271
      val reader = isabelle_system.fifo_reader(fifo)
wenzelm@28045
   272
      var kind: Kind.Value = null
wenzelm@28045
   273
      var props: Properties = null
wenzelm@28045
   274
      var result = new StringBuilder
wenzelm@27949
   275
wenzelm@27949
   276
      var finished = false
wenzelm@27949
   277
      while (!finished) {
wenzelm@27949
   278
        try {
wenzelm@28063
   279
          if (kind == null) {
wenzelm@28063
   280
            //{{{ Char mode -- resync
wenzelm@28063
   281
            var c = -1
wenzelm@28063
   282
            do {
wenzelm@28063
   283
              c = reader.read
wenzelm@28063
   284
              if (c >= 0 && c != 2) result.append(c.asInstanceOf[Char])
wenzelm@28063
   285
            } while (c >= 0 && c != 2)
wenzelm@28063
   286
wenzelm@28063
   287
            if (result.length > 0) {
wenzelm@28063
   288
              put_result(Kind.SYSTEM, null, "Malformed message:\n" + result.toString)
wenzelm@28063
   289
              result.length = 0
wenzelm@28063
   290
            }
wenzelm@28063
   291
            if (c < 0) {
wenzelm@28063
   292
              reader.close
wenzelm@28063
   293
              finished = true
wenzelm@28063
   294
              try_close()
wenzelm@28045
   295
            }
wenzelm@28045
   296
            else {
wenzelm@28344
   297
              c = reader.read
wenzelm@28344
   298
              if (Kind.code.isDefinedAt(c)) kind = Kind.code(c)
wenzelm@28344
   299
              else kind = null
wenzelm@28063
   300
              props = null
wenzelm@28063
   301
            }
wenzelm@28063
   302
            //}}}
wenzelm@28063
   303
          }
wenzelm@28063
   304
          else {
wenzelm@28063
   305
            //{{{ Line mode
wenzelm@28063
   306
            val line = reader.readLine
wenzelm@28063
   307
            if (line == null) {
wenzelm@28063
   308
              reader.close
wenzelm@28063
   309
              finished = true
wenzelm@28063
   310
              try_close()
wenzelm@28063
   311
            }
wenzelm@28063
   312
            else {
wenzelm@28063
   313
              val len = line.length
wenzelm@28063
   314
              // property
wenzelm@28063
   315
              if (line.endsWith("\u0002,")) {
wenzelm@28063
   316
                val i = line.indexOf('=')
wenzelm@28063
   317
                if (i > 0) {
wenzelm@28063
   318
                  val name = line.substring(0, i)
wenzelm@28063
   319
                  val value = line.substring(i + 1, len - 2)
wenzelm@28063
   320
                  if (props == null) props = new Properties
wenzelm@28063
   321
                  if (!props.containsKey(name)) props.setProperty(name, value)
wenzelm@28045
   322
                }
wenzelm@28045
   323
              }
wenzelm@28063
   324
              // last text line
wenzelm@28063
   325
              else if (line.endsWith("\u0002.")) {
wenzelm@28063
   326
                result.append(line.substring(0, len - 2))
wenzelm@28063
   327
                put_result(kind, props, result.toString)
wenzelm@28063
   328
                result.length = 0
wenzelm@28063
   329
                kind = null
wenzelm@28063
   330
              }
wenzelm@28063
   331
              // text line
wenzelm@28063
   332
              else {
wenzelm@28063
   333
                result.append(line)
wenzelm@28063
   334
                result.append('\n')
wenzelm@28063
   335
              }
wenzelm@28045
   336
            }
wenzelm@28063
   337
            //}}}
wenzelm@27949
   338
          }
wenzelm@27963
   339
        }
wenzelm@28063
   340
        catch {
wenzelm@28063
   341
          case e: IOException => put_result(Kind.SYSTEM, null, "Message thread: " + e.getMessage)
wenzelm@28063
   342
        }
wenzelm@27949
   343
      }
wenzelm@28063
   344
      put_result(Kind.SYSTEM, null, "Message thread terminated")
wenzelm@27949
   345
    }
wenzelm@27949
   346
  }
wenzelm@27949
   347
wenzelm@27949
   348
wenzelm@29192
   349
wenzelm@27949
   350
  /** main **/
wenzelm@27949
   351
wenzelm@27949
   352
  {
wenzelm@28497
   353
    /* isabelle version */
wenzelm@28497
   354
wenzelm@28497
   355
    {
wenzelm@29174
   356
      val (msg, rc) = isabelle_system.isabelle_tool("version")
wenzelm@28497
   357
      if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
wenzelm@28497
   358
      put_result(Kind.SYSTEM, null, msg)
wenzelm@28497
   359
    }
wenzelm@28497
   360
wenzelm@28045
   361
wenzelm@29192
   362
    /* messages */
wenzelm@28045
   363
wenzelm@29174
   364
    val message_fifo = isabelle_system.mk_fifo()
wenzelm@29174
   365
    def rm_fifo() = isabelle_system.rm_fifo(message_fifo)
wenzelm@28045
   366
wenzelm@28063
   367
    val message_thread = new MessageThread(message_fifo)
wenzelm@28063
   368
    message_thread.start
wenzelm@28045
   369
wenzelm@29194
   370
    new ResultThread().start
wenzelm@29194
   371
wenzelm@28045
   372
wenzelm@27973
   373
    /* exec process */
wenzelm@27963
   374
wenzelm@27973
   375
    try {
wenzelm@28501
   376
      val cmdline =
wenzelm@29174
   377
        List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
wenzelm@29178
   378
      proc = isabelle_system.execute(true, cmdline: _*)
wenzelm@27949
   379
    }
wenzelm@27993
   380
    catch {
wenzelm@28063
   381
      case e: IOException =>
wenzelm@28063
   382
        rm_fifo()
wenzelm@28063
   383
        error("Failed to execute Isabelle process: " + e.getMessage)
wenzelm@27993
   384
    }
wenzelm@27949
   385
wenzelm@27949
   386
wenzelm@28045
   387
    /* stdin/stdout */
wenzelm@28045
   388
wenzelm@28045
   389
    new StdinThread(proc.getOutputStream).start
wenzelm@28045
   390
    new StdoutThread(proc.getInputStream).start
wenzelm@28045
   391
wenzelm@28045
   392
wenzelm@28045
   393
    /* exit */
wenzelm@27949
   394
wenzelm@28063
   395
    new Thread("isabelle: exit") {
wenzelm@28045
   396
      override def run() = {
wenzelm@28045
   397
        val rc = proc.waitFor()
wenzelm@28045
   398
        Thread.sleep(300)
wenzelm@28045
   399
        put_result(Kind.SYSTEM, null, "Exit thread terminated")
wenzelm@28045
   400
        put_result(Kind.EXIT, null, Integer.toString(rc))
wenzelm@28063
   401
        rm_fifo()
wenzelm@28045
   402
      }
wenzelm@28063
   403
    }.start
wenzelm@28063
   404
wenzelm@27949
   405
  }
wenzelm@27949
   406
}