src/Pure/System/isabelle_process.scala
author wenzelm
Mon, 20 Sep 2010 21:20:06 +0200
changeset 39572 bb3469024b6a
parent 39530 16adc476348f
child 39573 a874ca3f5474
permissions -rw-r--r--
added Isabelle_Process.syslog; refined Isabelle_Process.process_manager: startup_output via syslog, explicit join of auxiliary threads; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30173
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29648
diff changeset
     1
/*  Title:      Pure/System/isabelle_process.ML
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
27963
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
     3
    Options:    :folding=explicit:collapseFolds=1:
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     4
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     5
Isabelle process management -- always reactive due to multi-threaded I/O.
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     6
*/
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     7
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     8
package isabelle
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
     9
27955
4c32c5e75eca use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
wenzelm
parents: 27949
diff changeset
    10
import java.util.concurrent.LinkedBlockingQueue
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
    11
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
    12
  InputStream, OutputStream, BufferedOutputStream, IOException}
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    13
32474
0818e6b1c8a6 Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents: 32448
diff changeset
    14
import scala.actors.Actor
0818e6b1c8a6 Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents: 32448
diff changeset
    15
import Actor._
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
    16
import scala.collection.mutable
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    17
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
    18
32474
0818e6b1c8a6 Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents: 32448
diff changeset
    19
object Isabelle_Process
0818e6b1c8a6 Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents: 32448
diff changeset
    20
{
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    21
  /* results */
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    22
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
    23
  object Kind
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
    24
  {
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
    25
    val message_markup = Map(
37689
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
    26
      ('A' : Int) -> Markup.INIT,
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
    27
      ('B' : Int) -> Markup.STATUS,
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 38231
diff changeset
    28
      ('C' : Int) -> Markup.REPORT,
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 38231
diff changeset
    29
      ('D' : Int) -> Markup.WRITELN,
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 38231
diff changeset
    30
      ('E' : Int) -> Markup.TRACING,
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 38231
diff changeset
    31
      ('F' : Int) -> Markup.WARNING,
39513
fce2202892c4 discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm
parents: 39439
diff changeset
    32
      ('G' : Int) -> Markup.ERROR)
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    33
  }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    34
37689
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
    35
  class Result(val message: XML.Elem)
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    36
  {
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37712
diff changeset
    37
    def kind = message.markup.name
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37712
diff changeset
    38
    def properties = message.markup.properties
37689
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
    39
    def body = message.body
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
    40
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
    41
    def is_init = kind == Markup.INIT
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
    42
    def is_exit = kind == Markup.EXIT
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
    43
    def is_stdout = kind == Markup.STDOUT
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
    44
    def is_system = kind == Markup.SYSTEM
37689
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
    45
    def is_status = kind == Markup.STATUS
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 38231
diff changeset
    46
    def is_report = kind == Markup.REPORT
38231
968844caaff9 simplified some Markup;
wenzelm
parents: 38230
diff changeset
    47
    def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil))
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    48
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    49
    override def toString: String =
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    50
    {
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    51
      val res =
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 38231
diff changeset
    52
        if (is_status || is_report) message.body.map(_.toString).mkString
37689
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
    53
        else Pretty.string_of(message.body)
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37712
diff changeset
    54
      if (properties.isEmpty)
29572
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
    55
        kind.toString + " [[" + res + "]]"
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
    56
      else
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
    57
        kind.toString + " " +
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37712
diff changeset
    58
          (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    59
    }
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
    60
  }
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
    61
}
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
    62
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
    63
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    64
class Isabelle_Process(system: Isabelle_System, timeout: Int, receiver: Actor, args: String*)
29192
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29178
diff changeset
    65
{
31797
203d5e61e3bc renamed IsabelleProcess to Isabelle_Process;
wenzelm
parents: 31498
diff changeset
    66
  import Isabelle_Process._
29194
wenzelm
parents: 29192
diff changeset
    67
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
    68
29192
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29178
diff changeset
    69
  /* demo constructor */
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
    70
29192
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29178
diff changeset
    71
  def this(args: String*) =
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    72
    this(new Isabelle_System, 10000,
34213
9e86c1ca6e51 removed obsolete version check -- sanity delegated to Isabelle_System;
wenzelm
parents: 34201
diff changeset
    73
      actor { loop { react { case res => Console.println(res) } } }, args: _*)
29174
d4058295affb proper class IsabelleSystem -- no longer static;
wenzelm
parents: 29140
diff changeset
    74
d4058295affb proper class IsabelleSystem -- no longer static;
wenzelm
parents: 29140
diff changeset
    75
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    76
  /* input actors */
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    77
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    78
  private case class Input_Text(text: String)
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    79
  private case class Input_Chunks(chunks: List[Array[Byte]])
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    80
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    81
  private case object Close
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    82
  private def close(a: Actor) { if (a != null) a ! Close }
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    83
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    84
  @volatile private var standard_input: Actor = null
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    85
  @volatile private var command_input: Actor = null
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    86
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    87
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    88
  /* process manager */
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    89
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    90
  private val in_fifo = system.mk_fifo()
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    91
  private val out_fifo = system.mk_fifo()
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    92
  private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    93
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    94
  private val proc =
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    95
    try {
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    96
      val cmdline =
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    97
        List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    98
      system.execute(true, cmdline: _*)
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
    99
    }
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   100
    catch { case e: IOException => rm_fifos(); throw(e) }
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   101
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   102
  private val stdout_reader =
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   103
    new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   104
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   105
  private val stdin_writer =
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   106
    new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   107
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   108
  private val (process_manager, _) = Simple_Thread.actor("process_manager")
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   109
  {
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   110
    val (startup_failed, startup_output) =
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   111
    {
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   112
      val expired = System.currentTimeMillis() + timeout
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   113
      val result = new StringBuilder(100)
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   114
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   115
      var finished = false
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   116
      while (!finished && System.currentTimeMillis() <= expired) {
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   117
        while (!finished && stdout_reader.ready) {
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   118
          val c = stdout_reader.read
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   119
          if (c == 2) finished = true
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   120
          else result += c.toChar
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   121
        }
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   122
        Thread.sleep(10)
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   123
      }
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   124
      (!finished, result.toString)
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   125
    }
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   126
    system_result(startup_output)
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   127
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   128
    if (startup_failed) {
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   129
      put_result(Markup.EXIT, "127")
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   130
      stdin_writer.close
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   131
      Thread.sleep(300)  // FIXME !?
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   132
      proc.destroy  // FIXME unreliable
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   133
    }
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   134
    else {
39530
16adc476348f Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents: 39528
diff changeset
   135
      // rendezvous
16adc476348f Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents: 39528
diff changeset
   136
      val command_stream = system.fifo_output_stream(in_fifo)
16adc476348f Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents: 39528
diff changeset
   137
      val message_stream = system.fifo_input_stream(out_fifo)
16adc476348f Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents: 39528
diff changeset
   138
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   139
      val stdin = stdin_actor(); standard_input = stdin._2
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   140
      val stdout = stdout_actor()
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   141
      val input = input_actor(command_stream); command_input = input._2
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   142
      val message = message_actor(message_stream)
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   143
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   144
      val rc = proc.waitFor()
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   145
      system_result("Isabelle process terminated")
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   146
      for ((thread, _) <- List(stdin, stdout, input, message)) thread.join
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   147
      system_result("process_manager terminated")
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   148
      put_result(Markup.EXIT, rc.toString)
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   149
    }
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   150
    rm_fifos()
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   151
  }
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   152
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   153
  def join() { process_manager.join() }
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   154
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   155
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   156
  /* system log */
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   157
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   158
  private val system_results = new mutable.ListBuffer[String]
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   159
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   160
  private def system_result(text: String)
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   161
  {
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   162
    synchronized { system_results += text }
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   163
    receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   164
  }
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   165
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   166
  def syslog(): List[String] = synchronized { system_results.toList }
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   167
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   168
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   169
  /* results */
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   170
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38445
diff changeset
   171
  private val xml_cache = new XML.Cache(131071)
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38445
diff changeset
   172
38573
d163f0f28e8c tuned signatures;
wenzelm
parents: 38446
diff changeset
   173
  private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
29572
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
   174
  {
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   175
    if (pid.isEmpty && kind == Markup.INIT) {
39530
16adc476348f Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents: 39528
diff changeset
   176
      rm_fifos()
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   177
      props.find(_._1 == Markup.PID).map(_._1) match {
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   178
        case None => system_result("Bad Isabelle process initialization: missing pid")
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   179
        case p => pid = p
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   180
      }
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   181
    }
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38445
diff changeset
   182
39439
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 38636
diff changeset
   183
    val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
1c294d150ded eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents: 38636
diff changeset
   184
    xml_cache.cache_tree(msg)((message: XML.Tree) =>
38446
9d59dab38fef XML.Cache: pipe-lined (thread-safe) version using actor;
wenzelm
parents: 38445
diff changeset
   185
      receiver ! new Result(message.asInstanceOf[XML.Elem]))
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   186
  }
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   187
37689
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
   188
  private def put_result(kind: String, text: String)
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   189
  {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   190
    put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
27992
131f7ea9e6e6 added try_result;
wenzelm
parents: 27990
diff changeset
   191
  }
131f7ea9e6e6 added try_result;
wenzelm
parents: 27990
diff changeset
   192
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   193
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   194
  /* signals */
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   195
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   196
  @volatile private var pid: Option[String] = None
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   197
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   198
  def interrupt()
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   199
  {
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   200
    pid match {
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   201
      case None => system_result("Cannot interrupt Isabelle: unknowd pid")
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   202
      case Some(i) =>
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   203
        try {
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   204
          if (system.execute(true, "kill", "-INT", i).waitFor == 0)
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   205
            system_result("Interrupt Isabelle")
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   206
          else
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   207
            system_result("Cannot interrupt Isabelle: kill command failed")
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   208
        }
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   209
        catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   210
    }
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   211
  }
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   212
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   213
  def kill()
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   214
  {
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   215
    val running =
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   216
      try { proc.exitValue; false }
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   217
      catch { case e: java.lang.IllegalThreadStateException => true }
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   218
    if (running) {
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   219
      close()
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   220
      Thread.sleep(500)  // FIXME !?
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   221
      system_result("Kill Isabelle")
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   222
      proc.destroy
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   223
    }
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   224
  }
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   225
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   226
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   227
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   228
  /** stream actors **/
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   229
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   230
  /* raw stdin */
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   231
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   232
  private def stdin_actor(): (Thread, Actor) =
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   233
  {
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   234
    val name = "standard_input"
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents: 38573
diff changeset
   235
    Simple_Thread.actor(name) {
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   236
      var finished = false
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   237
      while (!finished) {
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   238
        try {
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   239
          //{{{
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   240
          receive {
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   241
            case Input_Text(text) =>
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   242
              stdin_writer.write(text)
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   243
              stdin_writer.flush
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   244
            case Close =>
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   245
              stdin_writer.close
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   246
              finished = true
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   247
            case bad => System.err.println(name + ": ignoring bad message " + bad)
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   248
          }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   249
          //}}}
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   250
        }
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   251
        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   252
      }
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   253
      system_result(name + " terminated")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   254
    }
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   255
  }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   256
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   257
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   258
  /* raw stdout */
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   259
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   260
  private def stdout_actor(): (Thread, Actor) =
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   261
  {
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   262
    val name = "standard_output"
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents: 38573
diff changeset
   263
    Simple_Thread.actor(name) {
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   264
      var result = new StringBuilder(100)
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   265
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   266
      var finished = false
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   267
      while (!finished) {
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   268
        try {
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   269
          //{{{
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   270
          var c = -1
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   271
          var done = false
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   272
          while (!done && (result.length == 0 || stdout_reader.ready)) {
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   273
            c = stdout_reader.read
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   274
            if (c >= 0) result.append(c.asInstanceOf[Char])
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   275
            else done = true
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   276
          }
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   277
          if (result.length > 0) {
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   278
            put_result(Markup.STDOUT, result.toString)
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   279
            result.length = 0
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   280
          }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   281
          else {
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   282
            stdout_reader.close
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   283
            finished = true
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   284
          }
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   285
          //}}}
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   286
        }
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   287
        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   288
      }
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   289
      system_result(name + " terminated")
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   290
    }
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   291
  }
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   292
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   293
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   294
  /* command input */
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   295
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   296
  private def input_actor(raw_stream: OutputStream): (Thread, Actor) =
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   297
  {
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   298
    val name = "command_input"
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents: 38573
diff changeset
   299
    Simple_Thread.actor(name) {
39530
16adc476348f Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents: 39528
diff changeset
   300
      val stream = new BufferedOutputStream(raw_stream)
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   301
      var finished = false
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   302
      while (!finished) {
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   303
        try {
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   304
          //{{{
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   305
          receive {
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   306
            case Input_Chunks(chunks) =>
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   307
              stream.write(Standard_System.string_bytes(
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   308
                  chunks.map(_.length).mkString("", ",", "\n")));
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   309
              chunks.foreach(stream.write(_));
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   310
              stream.flush
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   311
            case Close =>
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   312
              stream.close
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   313
              finished = true
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   314
            case bad => System.err.println(name + ": ignoring bad message " + bad)
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   315
          }
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   316
          //}}}
27963
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
   317
        }
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   318
        catch { case e: IOException => system_result(name + ": " + e.getMessage) }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   319
      }
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   320
      system_result(name + " terminated")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   321
    }
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   322
  }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   323
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   324
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   325
  /* message output */
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   326
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   327
  private def message_actor(stream: InputStream): (Thread, Actor) =
39526
f1296795a8dc message_actor: more robust treatment of EOF;
wenzelm
parents: 39525
diff changeset
   328
  {
f1296795a8dc message_actor: more robust treatment of EOF;
wenzelm
parents: 39525
diff changeset
   329
    class EOF extends Exception
f1296795a8dc message_actor: more robust treatment of EOF;
wenzelm
parents: 39525
diff changeset
   330
    class Protocol_Error(msg: String) extends Exception(msg)
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   331
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   332
    val name = "message_output"
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents: 38573
diff changeset
   333
    Simple_Thread.actor(name) {
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   334
      val default_buffer = new Array[Byte](65536)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   335
      var c = -1
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   336
38573
d163f0f28e8c tuned signatures;
wenzelm
parents: 38446
diff changeset
   337
      def read_chunk(): XML.Body =
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   338
      {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   339
        //{{{
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   340
        // chunk size
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   341
        var n = 0
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   342
        c = stream.read
39526
f1296795a8dc message_actor: more robust treatment of EOF;
wenzelm
parents: 39525
diff changeset
   343
        if (c == -1) throw new EOF
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   344
        while (48 <= c && c <= 57) {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   345
          n = 10 * n + (c - 48)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   346
          c = stream.read
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   347
        }
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   348
        if (c != 10) throw new Protocol_Error("bad message chunk header")
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   349
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   350
        // chunk content
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   351
        val buf =
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   352
          if (n <= default_buffer.size) default_buffer
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   353
          else new Array[Byte](n)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   354
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   355
        var i = 0
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   356
        var m = 0
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   357
        do {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   358
          m = stream.read(buf, i, n - i)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   359
          i += m
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   360
        } while (m > 0 && n > i)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   361
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   362
        if (i != n) throw new Protocol_Error("bad message chunk content")
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   363
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   364
        YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n))
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   365
        //}}}
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   366
      }
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   367
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   368
      do {
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   369
        try {
38445
ba9ea6b9b75c simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents: 38372
diff changeset
   370
          val header = read_chunk()
ba9ea6b9b75c simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents: 38372
diff changeset
   371
          val body = read_chunk()
ba9ea6b9b75c simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents: 38372
diff changeset
   372
          header match {
ba9ea6b9b75c simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents: 38372
diff changeset
   373
            case List(XML.Elem(Markup(name, props), Nil))
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   374
                if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   375
              put_result(Kind.message_markup(name(0)), props, body)
38445
ba9ea6b9b75c simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents: 38372
diff changeset
   376
            case _ => throw new Protocol_Error("bad header: " + header.toString)
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   377
          }
27963
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
   378
        }
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   379
        catch {
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   380
          case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   381
          case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage)
39526
f1296795a8dc message_actor: more robust treatment of EOF;
wenzelm
parents: 39525
diff changeset
   382
          case _: EOF =>
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   383
        }
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   384
      } while (c != -1)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   385
      stream.close
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   386
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   387
      system_result(name + " terminated")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   388
    }
39526
f1296795a8dc message_actor: more robust treatment of EOF;
wenzelm
parents: 39525
diff changeset
   389
  }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   390
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   391
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   392
  /** main methods **/
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   393
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   394
  def input_raw(text: String): Unit = standard_input ! Input_Text(text)
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   395
38372
e753f71b6b34 added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);
wenzelm
parents: 38270
diff changeset
   396
  def input_bytes(name: String, args: Array[Byte]*): Unit =
e753f71b6b34 added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);
wenzelm
parents: 38270
diff changeset
   397
    command_input ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
e753f71b6b34 added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);
wenzelm
parents: 38270
diff changeset
   398
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   399
  def input(name: String, args: String*): Unit =
38372
e753f71b6b34 added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);
wenzelm
parents: 38270
diff changeset
   400
    input_bytes(name, args.map(Standard_System.string_bytes): _*)
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   401
39528
c01d89d18ff0 refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents: 39526
diff changeset
   402
  def close(): Unit = { close(command_input); close(standard_input) }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   403
}