src/Pure/System/isabelle_process.scala
author wenzelm
Wed, 22 Sep 2010 13:47:48 +0200
changeset 39585 00be8711082f
parent 39575 c77b9374f45c
child 39587 f84b70e3bb9c
permissions -rw-r--r--
main Isabelle_Process via Isabelle_System.Managed_Process; simplified init message: no pid; misc tuning and simplification;
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
39573
wenzelm
parents: 39572
diff changeset
    76
  /* system log */
wenzelm
parents: 39572
diff changeset
    77
wenzelm
parents: 39572
diff changeset
    78
  private val system_results = new mutable.ListBuffer[String]
wenzelm
parents: 39572
diff changeset
    79
wenzelm
parents: 39572
diff changeset
    80
  private def system_result(text: String)
wenzelm
parents: 39572
diff changeset
    81
  {
wenzelm
parents: 39572
diff changeset
    82
    synchronized { system_results += text }
wenzelm
parents: 39572
diff changeset
    83
    receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
wenzelm
parents: 39572
diff changeset
    84
  }
wenzelm
parents: 39572
diff changeset
    85
wenzelm
parents: 39572
diff changeset
    86
  def syslog(): List[String] = synchronized { system_results.toList }
wenzelm
parents: 39572
diff changeset
    87
wenzelm
parents: 39572
diff changeset
    88
wenzelm
parents: 39572
diff changeset
    89
  /* results */
wenzelm
parents: 39572
diff changeset
    90
wenzelm
parents: 39572
diff changeset
    91
  private val xml_cache = new XML.Cache(131071)
wenzelm
parents: 39572
diff changeset
    92
wenzelm
parents: 39572
diff changeset
    93
  private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
wenzelm
parents: 39572
diff changeset
    94
  {
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
    95
    if (kind == Markup.INIT) rm_fifos()
39573
wenzelm
parents: 39572
diff changeset
    96
    val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
wenzelm
parents: 39572
diff changeset
    97
    xml_cache.cache_tree(msg)((message: XML.Tree) =>
wenzelm
parents: 39572
diff changeset
    98
      receiver ! new Result(message.asInstanceOf[XML.Elem]))
wenzelm
parents: 39572
diff changeset
    99
  }
wenzelm
parents: 39572
diff changeset
   100
wenzelm
parents: 39572
diff changeset
   101
  private def put_result(kind: String, text: String)
wenzelm
parents: 39572
diff changeset
   102
  {
wenzelm
parents: 39572
diff changeset
   103
    put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
wenzelm
parents: 39572
diff changeset
   104
  }
wenzelm
parents: 39572
diff changeset
   105
wenzelm
parents: 39572
diff changeset
   106
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
   107
  /* 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
   108
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
   109
  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
   110
  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
   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
  private case object Close
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   113
  private def close(p: (Thread, Actor))
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   114
  {
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   115
    if (p != null && p._1.isAlive) {
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   116
      p._2 ! Close
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   117
      p._1.join
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   118
    }
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   119
  }
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
   120
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   121
  @volatile private var standard_input: (Thread, Actor) = null
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   122
  @volatile private var command_input: (Thread, Actor) = null
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
   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
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   125
  /** process manager **/
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
   126
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
   127
  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
   128
  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
   129
  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
   130
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   131
  private val process =
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
   132
    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
   133
      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
   134
        List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   135
      new system.Managed_Process(true, cmdline: _*)
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
   136
    }
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
   137
    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
   138
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   139
  private def terminate_process()
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   140
  {
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   141
    try { process.terminate }
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   142
    catch { case e: IOException => system_result("Failed to terminate Isabelle: " + e.getMessage) }
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   143
  }
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
   144
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   145
  private val process_manager = Simple_Thread.fork("process_manager")
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   146
  {
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
   147
    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
   148
    {
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
      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
   150
      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
   151
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
   152
      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
   153
      while (!finished && System.currentTimeMillis() <= expired) {
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   154
        while (!finished && process.stdout.ready) {
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   155
          val c = process.stdout.read
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
   156
          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
   157
          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
   158
        }
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
   159
        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
   160
      }
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
   161
      (!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
   162
    }
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   163
    system_result(startup_output)
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   164
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
   165
    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
   166
      put_result(Markup.EXIT, "127")
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   167
      process.stdin.close
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   168
      Thread.sleep(300)
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   169
      terminate_process()
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
   170
    }
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
   171
    else {
39530
16adc476348f Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents: 39528
diff changeset
   172
      // rendezvous
16adc476348f Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents: 39528
diff changeset
   173
      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
   174
      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
   175
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   176
      standard_input = stdin_actor()
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   177
      val stdout = stdout_actor()
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   178
      command_input = input_actor(command_stream)
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   179
      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
   180
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   181
      val rc = process.join
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
   182
      system_result("Isabelle process terminated")
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   183
      for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   184
      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
   185
      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
   186
    }
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
   187
    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
   188
  }
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   189
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   190
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   191
  /* management methods */
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   192
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   193
  def join() { process_manager.join() }
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
   194
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   195
  def interrupt()
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   196
  {
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   197
    try { process.interrupt }
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   198
    catch { case e: IOException => system_result("Failed to interrupt Isabelle: " + e.getMessage) }
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   199
  }
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   200
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   201
  def terminate()
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   202
  {
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   203
    close()
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   204
    system_result("Terminating Isabelle process")
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   205
    terminate_process()
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   206
  }
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   207
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   208
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   209
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   210
  /** stream actors **/
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   211
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   212
  /* raw stdin */
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   213
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   214
  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
   215
  {
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
    val name = "standard_input"
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents: 38573
diff changeset
   217
    Simple_Thread.actor(name) {
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   218
      var finished = false
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   219
      while (!finished) {
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   220
        try {
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   221
          //{{{
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   222
          receive {
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   223
            case Input_Text(text) =>
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   224
              process.stdin.write(text)
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   225
              process.stdin.flush
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   226
            case Close =>
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   227
              process.stdin.close
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   228
              finished = true
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   229
            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
   230
          }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   231
          //}}}
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   232
        }
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   233
        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
   234
      }
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   235
      system_result(name + " terminated")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   236
    }
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
   237
  }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   238
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   239
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   240
  /* raw stdout */
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   241
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   242
  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
   243
  {
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
   244
    val name = "standard_output"
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents: 38573
diff changeset
   245
    Simple_Thread.actor(name) {
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   246
      var result = new StringBuilder(100)
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   247
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   248
      var finished = false
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   249
      while (!finished) {
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   250
        try {
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   251
          //{{{
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   252
          var c = -1
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   253
          var done = false
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   254
          while (!done && (result.length == 0 || process.stdout.ready)) {
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   255
            c = process.stdout.read
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   256
            if (c >= 0) result.append(c.asInstanceOf[Char])
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   257
            else done = true
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   258
          }
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   259
          if (result.length > 0) {
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   260
            put_result(Markup.STDOUT, result.toString)
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   261
            result.length = 0
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   262
          }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   263
          else {
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   264
            process.stdout.close
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   265
            finished = true
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   266
          }
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   267
          //}}}
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   268
        }
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   269
        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
   270
      }
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   271
      system_result(name + " terminated")
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   272
    }
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
   273
  }
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   274
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   275
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   276
  /* command input */
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   277
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   278
  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
   279
  {
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
   280
    val name = "command_input"
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents: 38573
diff changeset
   281
    Simple_Thread.actor(name) {
39530
16adc476348f Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents: 39528
diff changeset
   282
      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
   283
      var finished = false
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   284
      while (!finished) {
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   285
        try {
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   286
          //{{{
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   287
          receive {
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   288
            case Input_Chunks(chunks) =>
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   289
              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
   290
                  chunks.map(_.length).mkString("", ",", "\n")));
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   291
              chunks.foreach(stream.write(_));
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   292
              stream.flush
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   293
            case Close =>
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   294
              stream.close
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   295
              finished = true
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   296
            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
   297
          }
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
   298
          //}}}
27963
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
   299
        }
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   300
        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
   301
      }
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   302
      system_result(name + " terminated")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   303
    }
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
   304
  }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   305
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   306
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   307
  /* message output */
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   308
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   309
  private def message_actor(stream: InputStream): (Thread, Actor) =
39526
f1296795a8dc message_actor: more robust treatment of EOF;
wenzelm
parents: 39525
diff changeset
   310
  {
f1296795a8dc message_actor: more robust treatment of EOF;
wenzelm
parents: 39525
diff changeset
   311
    class EOF extends Exception
f1296795a8dc message_actor: more robust treatment of EOF;
wenzelm
parents: 39525
diff changeset
   312
    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
   313
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
   314
    val name = "message_output"
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents: 38573
diff changeset
   315
    Simple_Thread.actor(name) {
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   316
      val default_buffer = new Array[Byte](65536)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   317
      var c = -1
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   318
38573
d163f0f28e8c tuned signatures;
wenzelm
parents: 38446
diff changeset
   319
      def read_chunk(): XML.Body =
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   320
      {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   321
        //{{{
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   322
        // chunk size
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   323
        var n = 0
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   324
        c = stream.read
39526
f1296795a8dc message_actor: more robust treatment of EOF;
wenzelm
parents: 39525
diff changeset
   325
        if (c == -1) throw new EOF
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   326
        while (48 <= c && c <= 57) {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   327
          n = 10 * n + (c - 48)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   328
          c = stream.read
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   329
        }
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   330
        if (c != 10) throw new Protocol_Error("bad message chunk header")
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   331
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   332
        // chunk content
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   333
        val buf =
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   334
          if (n <= default_buffer.size) default_buffer
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   335
          else new Array[Byte](n)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   336
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   337
        var i = 0
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   338
        var m = 0
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   339
        do {
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   340
          m = stream.read(buf, i, n - i)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   341
          i += m
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   342
        } while (m > 0 && n > i)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   343
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   344
        if (i != n) throw new Protocol_Error("bad message chunk content")
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   345
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   346
        YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n))
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   347
        //}}}
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   348
      }
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   349
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   350
      do {
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   351
        try {
38445
ba9ea6b9b75c simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents: 38372
diff changeset
   352
          val header = read_chunk()
ba9ea6b9b75c simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents: 38372
diff changeset
   353
          val body = read_chunk()
ba9ea6b9b75c simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents: 38372
diff changeset
   354
          header match {
ba9ea6b9b75c simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents: 38372
diff changeset
   355
            case List(XML.Elem(Markup(name, props), Nil))
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   356
                if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   357
              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
   358
            case _ => throw new Protocol_Error("bad header: " + header.toString)
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   359
          }
27963
c9ea82444189 YXML.parse_failsafe;
wenzelm
parents: 27955
diff changeset
   360
        }
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   361
        catch {
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   362
          case e: IOException => system_result("Cannot read message:\n" + e.getMessage)
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   363
          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
   364
          case _: EOF =>
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   365
        }
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   366
      } while (c != -1)
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   367
      stream.close
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   368
39525
72e949a0425b simplified Isabelle_Process message kinds;
wenzelm
parents: 39524
diff changeset
   369
      system_result(name + " terminated")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   370
    }
39526
f1296795a8dc message_actor: more robust treatment of EOF;
wenzelm
parents: 39525
diff changeset
   371
  }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   372
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   373
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   374
  /** main methods **/
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   375
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   376
  def input_raw(text: String): Unit = standard_input._2 ! Input_Text(text)
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   377
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
   378
  def input_bytes(name: String, args: Array[Byte]*): Unit =
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   379
    command_input._2 ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
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
   380
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   381
  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
   382
    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
   383
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
   384
  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
   385
}