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