src/Pure/System/isabelle_process.scala
author wenzelm
Wed, 08 Aug 2012 12:33:40 +0200
changeset 48731 a45ba78abcc1
parent 48705 dd32321d6eef
child 49445 638cefe3ee99
permissions -rw-r--r--
more casual exit back to ML toplevel, to accomodate commit in SML/NJ which continues at the saved point;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43283
446e6621762d updated headers;
wenzelm
parents: 40848
diff changeset
     1
/*  Title:      Pure/System/isabelle_process.scala
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
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 43514
diff changeset
    10
import java.lang.System
27955
4c32c5e75eca use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
wenzelm
parents: 27949
diff changeset
    11
import java.util.concurrent.LinkedBlockingQueue
28045
1a6f273108ae join stdout/stderr, eliminated Kind.STDERR;
wenzelm
parents: 27999
diff changeset
    12
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
    13
  InputStream, OutputStream, BufferedOutputStream, IOException}
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    14
32474
0818e6b1c8a6 Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents: 32448
diff changeset
    15
import scala.actors.Actor
0818e6b1c8a6 Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents: 32448
diff changeset
    16
import Actor._
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
{
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
    21
  /* messages */
27949
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(
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    26
      ('A' : Int) -> Isabelle_Markup.INIT,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    27
      ('B' : Int) -> Isabelle_Markup.STATUS,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    28
      ('C' : Int) -> Isabelle_Markup.REPORT,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    29
      ('D' : Int) -> Isabelle_Markup.WRITELN,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    30
      ('E' : Int) -> Isabelle_Markup.TRACING,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    31
      ('F' : Int) -> Isabelle_Markup.WARNING,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    32
      ('G' : Int) -> Isabelle_Markup.ERROR,
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46773
diff changeset
    33
      ('H' : Int) -> Isabelle_Markup.PROTOCOL)
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    34
  }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
    35
44733
329320fc88df buffer prover messages to prevent overloading of session_actor input channel -- which is critical due to synchronous messages wrt. GUI thread;
wenzelm
parents: 44732
diff changeset
    36
  sealed abstract class Message
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43695
diff changeset
    37
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43695
diff changeset
    38
  class Input(name: String, args: List[String]) extends Message
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43695
diff changeset
    39
  {
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43695
diff changeset
    40
    override def toString: String =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    41
      XML.Elem(Markup(Isabelle_Markup.PROVER_COMMAND, List((Markup.NAME, name))),
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43695
diff changeset
    42
        args.map(s =>
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    43
          List(XML.Text("\n"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    44
            XML.elem(Isabelle_Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43695
diff changeset
    45
  }
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43695
diff changeset
    46
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
    47
  class Output(val message: XML.Elem) extends Message
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    48
  {
43747
74a9e9c8d5e8 tuned signature;
wenzelm
parents: 43746
diff changeset
    49
    def kind: String = message.markup.name
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    50
    def properties: Properties.T = message.markup.properties
43747
74a9e9c8d5e8 tuned signature;
wenzelm
parents: 43746
diff changeset
    51
    def body: XML.Body = message.body
37689
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
    52
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    53
    def is_init = kind == Isabelle_Markup.INIT
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    54
    def is_exit = kind == Isabelle_Markup.EXIT
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    55
    def is_stdout = kind == Isabelle_Markup.STDOUT
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    56
    def is_stderr = kind == Isabelle_Markup.STDERR
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    57
    def is_system = kind == Isabelle_Markup.SYSTEM
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    58
    def is_status = kind == Isabelle_Markup.STATUS
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    59
    def is_report = kind == Isabelle_Markup.REPORT
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46773
diff changeset
    60
    def is_protocol = kind == Isabelle_Markup.PROTOCOL
46121
30a69cd8a9a0 prefer raw_message for protocol implementation;
wenzelm
parents: 45709
diff changeset
    61
    def is_syslog = is_init || is_exit || is_system || is_stderr
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    62
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    63
    override def toString: String =
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
    64
    {
29522
793766d4c1b5 moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents: 29506
diff changeset
    65
      val res =
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 38231
diff changeset
    66
        if (is_status || is_report) message.body.map(_.toString).mkString
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46773
diff changeset
    67
        else if (is_protocol) "..."
37689
628eabe2213a simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents: 37132
diff changeset
    68
        else Pretty.string_of(message.body)
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37712
diff changeset
    69
      if (properties.isEmpty)
29572
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
    70
        kind.toString + " [[" + res + "]]"
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
    71
      else
e3a99d957392 replaced java.util.Properties by plain association list;
wenzelm
parents: 29522
diff changeset
    72
        kind.toString + " " +
38230
ed147003de4b simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents: 37712
diff changeset
    73
          (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
    74
    }
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
    75
  }
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
    76
}
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
    77
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
    78
45055
55274f7e306b explicit option for socket vs. fifo communication;
wenzelm
parents: 45027
diff changeset
    79
class Isabelle_Process(
55274f7e306b explicit option for socket vs. fifo communication;
wenzelm
parents: 45027
diff changeset
    80
    receiver: Isabelle_Process.Message => Unit = Console.println(_),
55274f7e306b explicit option for socket vs. fifo communication;
wenzelm
parents: 45027
diff changeset
    81
    args: List[String] = Nil)
29192
082ee2a01a6d explicit EventBus for results;
wenzelm
parents: 29178
diff changeset
    82
{
31797
203d5e61e3bc renamed IsabelleProcess to Isabelle_Process;
wenzelm
parents: 31498
diff changeset
    83
  import Isabelle_Process._
29194
wenzelm
parents: 29192
diff changeset
    84
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
    85
48705
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
    86
  /* text representation */
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
    87
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
    88
  def encode(s: String): String = Symbol.encode(s)
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
    89
  def decode(s: String): String = Symbol.decode(s)
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
    90
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
    91
  object Encode
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
    92
  {
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
    93
    val string: XML.Encode.T[String] = (s => XML.Encode.string(encode(s)))
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
    94
  }
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
    95
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
    96
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
    97
  /* output */
39573
wenzelm
parents: 39572
diff changeset
    98
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
    99
  private def system_output(text: String)
39573
wenzelm
parents: 39572
diff changeset
   100
  {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   101
    receiver(new Output(XML.Elem(Markup(Isabelle_Markup.SYSTEM, Nil), List(XML.Text(text)))))
39573
wenzelm
parents: 39572
diff changeset
   102
  }
wenzelm
parents: 39572
diff changeset
   103
43745
562e35bc351e tuned XML.Cache parameters;
wenzelm
parents: 43721
diff changeset
   104
  private val xml_cache = new XML.Cache()
39573
wenzelm
parents: 39572
diff changeset
   105
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   106
  private def output_message(kind: String, props: Properties.T, body: XML.Body)
39573
wenzelm
parents: 39572
diff changeset
   107
  {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
   108
    if (kind == Isabelle_Markup.INIT) system_channel.accepted()
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46773
diff changeset
   109
    if (kind == Isabelle_Markup.PROTOCOL)
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   110
      receiver(new Output(XML.Elem(Markup(kind, props), body)))
43746
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43745
diff changeset
   111
    else {
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
   112
      val msg = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   113
      receiver(new Output(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem]))
43746
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43745
diff changeset
   114
    }
39573
wenzelm
parents: 39572
diff changeset
   115
  }
wenzelm
parents: 39572
diff changeset
   116
48016
edbc8e8accd9 more explicit treatment of return code vs. session phase;
wenzelm
parents: 46774
diff changeset
   117
  private def exit_message(rc: Int)
39573
wenzelm
parents: 39572
diff changeset
   118
  {
48016
edbc8e8accd9 more explicit treatment of return code vs. session phase;
wenzelm
parents: 46774
diff changeset
   119
    output_message(Isabelle_Markup.EXIT, Isabelle_Markup.Return_Code(rc),
edbc8e8accd9 more explicit treatment of return code vs. session phase;
wenzelm
parents: 46774
diff changeset
   120
      List(XML.Text("Return code: " + rc.toString)))
39573
wenzelm
parents: 39572
diff changeset
   121
  }
wenzelm
parents: 39572
diff changeset
   122
wenzelm
parents: 39572
diff changeset
   123
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
   124
  /* 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
   125
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
  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
   127
  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
   128
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 case object Close
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   130
  private def close(p: (Thread, Actor))
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   131
  {
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   132
    if (p != null && p._1.isAlive) {
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   133
      p._2 ! Close
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   134
      p._1.join
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   135
    }
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   136
  }
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
   137
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   138
  @volatile private var standard_input: (Thread, Actor) = null
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   139
  @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
   140
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
   141
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   142
  /** 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
   143
45158
db4bf4fb5492 always use sockets on Windows/Cygwin;
wenzelm
parents: 45075
diff changeset
   144
  private val system_channel = System_Channel()
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
   145
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   146
  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
   147
    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
   148
      val cmdline =
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents: 44775
diff changeset
   149
        Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
45055
55274f7e306b explicit option for socket vs. fifo communication;
wenzelm
parents: 45027
diff changeset
   150
          (system_channel.isabelle_args ::: args)
48353
bcce872202b3 support external processes with explicit environment;
wenzelm
parents: 48020
diff changeset
   151
      new Isabelle_System.Managed_Process(null, null, false, 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
   152
    }
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents: 44775
diff changeset
   153
    catch { case e: IOException => system_channel.accepted(); throw(e) }
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
   154
48355
6b36da29a0bf support for detached Bash_Job with some control operations;
wenzelm
parents: 48353
diff changeset
   155
  val (_, process_result) =
39587
f84b70e3bb9c more reactive handling of Isabelle_Process startup errors;
wenzelm
parents: 39585
diff changeset
   156
    Simple_Thread.future("process_result") { process.join }
f84b70e3bb9c more reactive handling of Isabelle_Process startup errors;
wenzelm
parents: 39585
diff changeset
   157
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   158
  private def terminate_process()
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   159
  {
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   160
    try { process.terminate }
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   161
    catch { case e: IOException => system_output("Failed to terminate Isabelle: " + e.getMessage) }
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   162
  }
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
   163
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   164
  private val process_manager = Simple_Thread.fork("process_manager")
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   165
  {
46548
c54a4a22501c clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
wenzelm
parents: 46121
diff changeset
   166
    val (startup_failed, startup_errors) =
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
   167
    {
48020
a4f9957878ab clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents: 48019
diff changeset
   168
      var finished: Option[Boolean] = None
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
   169
      val result = new StringBuilder(100)
48020
a4f9957878ab clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents: 48019
diff changeset
   170
      while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
46548
c54a4a22501c clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
wenzelm
parents: 46121
diff changeset
   171
        while (finished.isEmpty && process.stderr.ready) {
48020
a4f9957878ab clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents: 48019
diff changeset
   172
          try {
a4f9957878ab clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents: 48019
diff changeset
   173
            val c = process.stderr.read
a4f9957878ab clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents: 48019
diff changeset
   174
            if (c == 2) finished = Some(true)
a4f9957878ab clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents: 48019
diff changeset
   175
            else result += c.toChar
a4f9957878ab clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents: 48019
diff changeset
   176
          }
a4f9957878ab clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents: 48019
diff changeset
   177
          catch { case _: IOException => finished = Some(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
   178
        }
48020
a4f9957878ab clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents: 48019
diff changeset
   179
        Thread.sleep(10)
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
      }
39623
6aae022fde9b tuned message;
wenzelm
parents: 39618
diff changeset
   181
      (finished.isEmpty || !finished.get, result.toString.trim)
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
    }
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   183
    if (startup_errors != "") system_output(startup_errors)
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   184
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
    if (startup_failed) {
48016
edbc8e8accd9 more explicit treatment of return code vs. session phase;
wenzelm
parents: 46774
diff changeset
   186
      exit_message(127)
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   187
      process.stdin.close
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   188
      Thread.sleep(300)
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   189
      terminate_process()
39587
f84b70e3bb9c more reactive handling of Isabelle_Process startup errors;
wenzelm
parents: 39585
diff changeset
   190
      process_result.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
   191
    }
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
   192
    else {
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents: 44775
diff changeset
   193
      val (command_stream, message_stream) = system_channel.rendezvous()
39530
16adc476348f Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents: 39528
diff changeset
   194
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   195
      standard_input = stdin_actor()
46773
wenzelm
parents: 46772
diff changeset
   196
      val stdout = physical_output_actor(false)
wenzelm
parents: 46772
diff changeset
   197
      val stderr = physical_output_actor(true)
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   198
      command_input = input_actor(command_stream)
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   199
      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
   200
39587
f84b70e3bb9c more reactive handling of Isabelle_Process startup errors;
wenzelm
parents: 39585
diff changeset
   201
      val rc = process_result.join
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   202
      system_output("process terminated")
48019
226dee06ab6e need to close_input before expecting threads to terminate/join;
wenzelm
parents: 48016
diff changeset
   203
      close_input()
45633
2cb7e34f6096 retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents: 45158
diff changeset
   204
      for ((thread, _) <- List(standard_input, stdout, stderr, command_input, message))
2cb7e34f6096 retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents: 45158
diff changeset
   205
        thread.join
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   206
      system_output("process_manager terminated")
48016
edbc8e8accd9 more explicit treatment of return code vs. session phase;
wenzelm
parents: 46774
diff changeset
   207
      exit_message(rc)
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
   208
    }
45027
f459e93a038e more abstract wrapping of fifos as System_Channel;
wenzelm
parents: 44775
diff changeset
   209
    system_channel.accepted()
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
   210
  }
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   211
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   212
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   213
  /* management methods */
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   214
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   215
  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
   216
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   217
  def terminate()
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   218
  {
48019
226dee06ab6e need to close_input before expecting threads to terminate/join;
wenzelm
parents: 48016
diff changeset
   219
    close_input()
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   220
    system_output("Terminating Isabelle process")
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   221
    terminate_process()
27973
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   222
  }
18d02c0b90b6 moved class Result into static object, removed dynamic tree method;
wenzelm
parents: 27963
diff changeset
   223
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   224
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   225
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   226
  /** stream actors **/
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   227
46773
wenzelm
parents: 46772
diff changeset
   228
  /* physical stdin */
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   229
39572
bb3469024b6a added Isabelle_Process.syslog;
wenzelm
parents: 39530
diff changeset
   230
  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
   231
  {
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
   232
    val name = "standard_input"
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents: 38573
diff changeset
   233
    Simple_Thread.actor(name) {
46769
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   234
      try {
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   235
        var finished = false
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   236
        while (!finished) {
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   237
          //{{{
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   238
          receive {
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   239
            case Input_Text(text) =>
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   240
              process.stdin.write(text)
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   241
              process.stdin.flush
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   242
            case Close =>
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   243
              process.stdin.close
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   244
              finished = true
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   245
            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
   246
          }
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
        }
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   249
      }
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   250
      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   251
      system_output(name + " terminated")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   252
    }
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
   253
  }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   254
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   255
46773
wenzelm
parents: 46772
diff changeset
   256
  /* physical output */
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   257
46773
wenzelm
parents: 46772
diff changeset
   258
  private def physical_output_actor(err: Boolean): (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
   259
  {
45633
2cb7e34f6096 retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents: 45158
diff changeset
   260
    val (name, reader, markup) =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
   261
      if (err) ("standard_error", process.stderr, Isabelle_Markup.STDERR)
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
   262
      else ("standard_output", process.stdout, Isabelle_Markup.STDOUT)
45633
2cb7e34f6096 retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents: 45158
diff changeset
   263
38636
b7647ca7de5a module for simplified thread operations (Scala version);
wenzelm
parents: 38573
diff changeset
   264
    Simple_Thread.actor(name) {
46769
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   265
      try {
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   266
        var result = new StringBuilder(100)
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   267
        var finished = false
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   268
        while (!finished) {
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
45633
2cb7e34f6096 retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents: 45158
diff changeset
   272
          while (!done && (result.length == 0 || reader.ready)) {
2cb7e34f6096 retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents: 45158
diff changeset
   273
            c = 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) {
48705
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
   278
            output_message(markup, Nil, List(XML.Text(decode(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 {
45633
2cb7e34f6096 retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents: 45158
diff changeset
   282
            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
        }
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   287
      }
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   288
      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   289
      system_output(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) {
46769
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   300
      try {
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   301
        val stream = new BufferedOutputStream(raw_stream)
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   302
        var finished = false
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   303
        while (!finished) {
38270
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
        }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   318
      }
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   319
      catch { case e: IOException => system_output(name + ": " + e.getMessage) }
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   320
      system_output(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
48705
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
   337
      def read_chunk(do_decode: Boolean): 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)
39731
5cb0d7b0d601 bulk read: observe EOF protocol more carefully -- 0 counts as successful read;
wenzelm
parents: 39632
diff changeset
   359
          if (m != -1) i += m
5cb0d7b0d601 bulk read: observe EOF protocol more carefully -- 0 counts as successful read;
wenzelm
parents: 39632
diff changeset
   360
        } while (m != -1 && n > i)
34100
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
48705
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
   364
        if (do_decode)
dd32321d6eef tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents: 48355
diff changeset
   365
          YXML.parse_body_failsafe(Standard_System.decode_chars(decode, buf, 0, n))
43746
a41f618c641d some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents: 43745
diff changeset
   366
        else List(XML.Text(Standard_System.decode_chars(s => s, buf, 0, n).toString))
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   367
        //}}}
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   368
      }
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   369
46769
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   370
      try {
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   371
        do {
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   372
          try {
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   373
            //{{{
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   374
            val header = read_chunk(true)
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   375
            header match {
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   376
              case List(XML.Elem(Markup(name, props), Nil))
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   377
                  if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) =>
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   378
                val kind = Kind.message_markup(name(0))
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46773
diff changeset
   379
                val body = read_chunk(kind != Isabelle_Markup.PROTOCOL)
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   380
                output_message(kind, props, body)
46769
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   381
              case _ =>
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   382
                read_chunk(false)
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   383
                throw new Protocol_Error("bad header: " + header.toString)
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   384
            }
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   385
            //}}}
28063
3533485fc7b8 IsabelleSystem.mk_fifo, IsabelleSystem.rm_fifo;
wenzelm
parents: 28056
diff changeset
   386
          }
46769
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   387
          catch { case _: EOF => }
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   388
        } while (c != -1)
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   389
      }
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   390
      catch {
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   391
        case e: IOException => system_output("Cannot read message:\n" + e.getMessage)
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   392
        case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage)
46769
0038386efd81 clarified scope of exception handlers;
wenzelm
parents: 46762
diff changeset
   393
      }
34100
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   394
      stream.close
ea24958c2af5 fifo: raw byte stream;
wenzelm
parents: 32474
diff changeset
   395
46772
be21f050eda4 tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents: 46769
diff changeset
   396
      system_output(name + " terminated")
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   397
    }
39526
f1296795a8dc message_actor: more robust treatment of EOF;
wenzelm
parents: 39525
diff changeset
   398
  }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   399
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   400
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   401
  /** main methods **/
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   402
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   403
  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
   404
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
   405
  def input_bytes(name: String, args: Array[Byte]*): Unit =
39585
00be8711082f main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents: 39575
diff changeset
   406
    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
   407
38270
71bb3c273dd1 native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents: 38262
diff changeset
   408
  def input(name: String, args: String*): Unit =
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43695
diff changeset
   409
  {
44732
c58b69d888ac more abstract receiver interface;
wenzelm
parents: 44705
diff changeset
   410
    receiver(new Input(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
   411
    input_bytes(name, args.map(Standard_System.string_bytes): _*)
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43695
diff changeset
   412
  }
38259
2b61c5e27399 distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents: 38253
diff changeset
   413
48019
226dee06ab6e need to close_input before expecting threads to terminate/join;
wenzelm
parents: 48016
diff changeset
   414
  def close_input(): Unit = { close(command_input); close(standard_input) }
27949
6eb0327c0b9b Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff changeset
   415
}