author | wenzelm |
Mon, 25 Nov 2013 18:03:38 +0100 | |
changeset 54645 | c19c83f49fa5 |
parent 54005 | 132640f4c453 |
child 54440 | 2c4940d2edf7 |
permissions | -rw-r--r-- |
43283 | 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 | 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 | 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 |
|
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
|
23 |
sealed abstract class Message |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
24 |
|
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
25 |
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
|
26 |
{ |
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
27 |
override def toString: String = |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
28 |
XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))), |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
29 |
args.map(s => |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
30 |
List(XML.Text("\n"), XML.elem(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
|
31 |
} |
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
32 |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
33 |
class Output(val message: XML.Elem) extends Message |
34100 | 34 |
{ |
43747 | 35 |
def kind: String = message.markup.name |
43780 | 36 |
def properties: Properties.T = message.markup.properties |
43747 | 37 |
def body: XML.Body = message.body |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
38 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
39 |
def is_init = kind == Markup.INIT |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
40 |
def is_exit = kind == Markup.EXIT |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
41 |
def is_stdout = kind == Markup.STDOUT |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
42 |
def is_stderr = kind == Markup.STDERR |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
43 |
def is_system = kind == Markup.SYSTEM |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
44 |
def is_status = kind == Markup.STATUS |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
45 |
def is_report = kind == Markup.REPORT |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
46 |
def is_protocol = kind == Markup.PROTOCOL |
46121 | 47 |
def is_syslog = is_init || is_exit || is_system || is_stderr |
34100 | 48 |
|
49 |
override def toString: String = |
|
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 |
46774 | 53 |
else if (is_protocol) "..." |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
54 |
else Pretty.string_of(message.body) |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37712
diff
changeset
|
55 |
if (properties.isEmpty) |
29572
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
56 |
kind.toString + " [[" + res + "]]" |
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
57 |
else |
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
58 |
kind.toString + " " + |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37712
diff
changeset
|
59 |
(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
|
60 |
} |
27973
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 |
|
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
64 |
|
45055
55274f7e306b
explicit option for socket vs. fifo communication;
wenzelm
parents:
45027
diff
changeset
|
65 |
class Isabelle_Process( |
55274f7e306b
explicit option for socket vs. fifo communication;
wenzelm
parents:
45027
diff
changeset
|
66 |
receiver: Isabelle_Process.Message => Unit = Console.println(_), |
54005
132640f4c453
tuned signature -- facilitate experimentation with other processes;
wenzelm
parents:
52799
diff
changeset
|
67 |
arguments: List[String] = Nil) |
29192 | 68 |
{ |
31797 | 69 |
import Isabelle_Process._ |
29194 | 70 |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
71 |
|
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
72 |
/* text representation */ |
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
73 |
|
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
74 |
def encode(s: String): String = Symbol.encode(s) |
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
75 |
def decode(s: String): String = Symbol.decode(s) |
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
76 |
|
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
77 |
object Encode |
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
78 |
{ |
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
79 |
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
|
80 |
} |
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
81 |
|
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
82 |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
83 |
/* output */ |
39573 | 84 |
|
51664 | 85 |
val xml_cache = new XML.Cache() |
86 |
||
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
87 |
private def system_output(text: String) |
39573 | 88 |
{ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
89 |
receiver(new Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))) |
39573 | 90 |
} |
91 |
||
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
92 |
private def output_message(kind: String, props: Properties.T, body: XML.Body) |
39573 | 93 |
{ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
94 |
if (kind == Markup.INIT) system_channel.accepted() |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
95 |
if (kind == Markup.PROTOCOL) |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
96 |
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
|
97 |
else { |
49445
638cefe3ee99
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents:
48705
diff
changeset
|
98 |
val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body)) |
638cefe3ee99
earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);
wenzelm
parents:
48705
diff
changeset
|
99 |
val reports = Protocol.message_reports(props, body) |
51663 | 100 |
for (msg <- main :: reports) receiver(new Output(xml_cache.elem(msg))) |
43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
101 |
} |
39573 | 102 |
} |
103 |
||
48016
edbc8e8accd9
more explicit treatment of return code vs. session phase;
wenzelm
parents:
46774
diff
changeset
|
104 |
private def exit_message(rc: Int) |
39573 | 105 |
{ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
106 |
output_message(Markup.EXIT, Markup.Return_Code(rc), |
48016
edbc8e8accd9
more explicit treatment of return code vs. session phase;
wenzelm
parents:
46774
diff
changeset
|
107 |
List(XML.Text("Return code: " + rc.toString))) |
39573 | 108 |
} |
109 |
||
110 |
||
52581 | 111 |
/* command input 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
|
112 |
|
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
113 |
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
|
114 |
|
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
115 |
private case object Close |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
116 |
private def close(p: (Thread, Actor)) |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
117 |
{ |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
118 |
if (p != null && p._1.isAlive) { |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
119 |
p._2 ! Close |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
120 |
p._1.join |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
121 |
} |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
122 |
} |
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 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
124 |
@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
|
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 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
127 |
/** 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
|
128 |
|
54005
132640f4c453
tuned signature -- facilitate experimentation with other processes;
wenzelm
parents:
52799
diff
changeset
|
129 |
def command_line(channel: System_Channel, args: List[String]): List[String] = |
132640f4c453
tuned signature -- facilitate experimentation with other processes;
wenzelm
parents:
52799
diff
changeset
|
130 |
Isabelle_System.getenv_strict("ISABELLE_PROCESS") :: (channel.isabelle_args ::: args) |
132640f4c453
tuned signature -- facilitate experimentation with other processes;
wenzelm
parents:
52799
diff
changeset
|
131 |
|
45158 | 132 |
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
|
133 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
134 |
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
|
135 |
try { |
54005
132640f4c453
tuned signature -- facilitate experimentation with other processes;
wenzelm
parents:
52799
diff
changeset
|
136 |
val cmdline = command_line(system_channel, arguments) |
48353
bcce872202b3
support external processes with explicit environment;
wenzelm
parents:
48020
diff
changeset
|
137 |
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
|
138 |
} |
45027
f459e93a038e
more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
44775
diff
changeset
|
139 |
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
|
140 |
|
48355
6b36da29a0bf
support for detached Bash_Job with some control operations;
wenzelm
parents:
48353
diff
changeset
|
141 |
val (_, process_result) = |
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
142 |
Simple_Thread.future("process_result") { process.join } |
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
143 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
144 |
private def terminate_process() |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
145 |
{ |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
146 |
try { process.terminate } |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
147 |
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
|
148 |
} |
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
|
149 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
150 |
private val process_manager = Simple_Thread.fork("process_manager") |
39572 | 151 |
{ |
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
|
152 |
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
|
153 |
{ |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
154 |
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
|
155 |
val result = new StringBuilder(100) |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
156 |
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
|
157 |
while (finished.isEmpty && process.stderr.ready) { |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
158 |
try { |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
159 |
val c = process.stderr.read |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
160 |
if (c == 2) finished = Some(true) |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
161 |
else result += c.toChar |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
162 |
} |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
163 |
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
|
164 |
} |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
165 |
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
|
166 |
} |
39623 | 167 |
(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
|
168 |
} |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
169 |
if (startup_errors != "") system_output(startup_errors) |
39572 | 170 |
|
52581 | 171 |
process.stdin.close |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
172 |
if (startup_failed) { |
48016
edbc8e8accd9
more explicit treatment of return code vs. session phase;
wenzelm
parents:
46774
diff
changeset
|
173 |
exit_message(127) |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
174 |
Thread.sleep(300) |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
175 |
terminate_process() |
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
176 |
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
|
177 |
} |
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 |
else { |
45027
f459e93a038e
more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
44775
diff
changeset
|
179 |
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
|
180 |
|
46773 | 181 |
val stdout = physical_output_actor(false) |
182 |
val stderr = physical_output_actor(true) |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
183 |
command_input = input_actor(command_stream) |
39572 | 184 |
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
|
185 |
|
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
186 |
val rc = process_result.join |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
187 |
system_output("process terminated") |
52581 | 188 |
close(command_input) |
189 |
for ((thread, _) <- List(stdout, stderr, command_input, message)) |
|
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
|
190 |
thread.join |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
191 |
system_output("process_manager terminated") |
48016
edbc8e8accd9
more explicit treatment of return code vs. session phase;
wenzelm
parents:
46774
diff
changeset
|
192 |
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
|
193 |
} |
45027
f459e93a038e
more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
44775
diff
changeset
|
194 |
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
|
195 |
} |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
196 |
|
39572 | 197 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
198 |
/* management methods */ |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
199 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
200 |
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
|
201 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
202 |
def terminate() |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
203 |
{ |
52581 | 204 |
close(command_input) |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
205 |
system_output("Terminating Isabelle process") |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
206 |
terminate_process() |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
207 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
208 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
209 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
210 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
211 |
/** stream actors **/ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
212 |
|
46773 | 213 |
/* physical output */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
214 |
|
46773 | 215 |
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
|
216 |
{ |
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
|
217 |
val (name, reader, markup) = |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
218 |
if (err) ("standard_error", process.stderr, Markup.STDERR) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
219 |
else ("standard_output", process.stdout, 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
|
220 |
|
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
38573
diff
changeset
|
221 |
Simple_Thread.actor(name) { |
46769 | 222 |
try { |
223 |
var result = new StringBuilder(100) |
|
224 |
var finished = false |
|
225 |
while (!finished) { |
|
28045 | 226 |
//{{{ |
227 |
var c = -1 |
|
228 |
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
|
229 |
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
|
230 |
c = reader.read |
28045 | 231 |
if (c >= 0) result.append(c.asInstanceOf[Char]) |
232 |
else done = true |
|
233 |
} |
|
234 |
if (result.length > 0) { |
|
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
235 |
output_message(markup, Nil, List(XML.Text(decode(result.toString)))) |
28045 | 236 |
result.length = 0 |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
237 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
238 |
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
|
239 |
reader.close |
28045 | 240 |
finished = true |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
241 |
} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
242 |
//}}} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
243 |
} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
244 |
} |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
245 |
catch { case e: IOException => system_output(name + ": " + e.getMessage) } |
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
246 |
system_output(name + " terminated") |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
247 |
} |
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
|
248 |
} |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
249 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
250 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
251 |
/* command input */ |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
252 |
|
39572 | 253 |
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
|
254 |
{ |
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
255 |
val name = "command_input" |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
38573
diff
changeset
|
256 |
Simple_Thread.actor(name) { |
46769 | 257 |
try { |
258 |
val stream = new BufferedOutputStream(raw_stream) |
|
259 |
var finished = false |
|
260 |
while (!finished) { |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
261 |
//{{{ |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
262 |
receive { |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
263 |
case Input_Chunks(chunks) => |
50203 | 264 |
stream.write(UTF8.string_bytes(chunks.map(_.length).mkString("", ",", "\n"))) |
265 |
chunks.foreach(stream.write(_)) |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
266 |
stream.flush |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
267 |
case Close => |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
268 |
stream.close |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
269 |
finished = true |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
270 |
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
|
271 |
} |
28045 | 272 |
//}}} |
27963 | 273 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
274 |
} |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
275 |
catch { case e: IOException => system_output(name + ": " + e.getMessage) } |
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
276 |
system_output(name + " terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
277 |
} |
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
|
278 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
279 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
280 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
281 |
/* message output */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
282 |
|
39572 | 283 |
private def message_actor(stream: InputStream): (Thread, Actor) = |
39526 | 284 |
{ |
285 |
class EOF extends Exception |
|
286 |
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
|
287 |
|
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
|
288 |
val name = "message_output" |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
38573
diff
changeset
|
289 |
Simple_Thread.actor(name) { |
34100 | 290 |
val default_buffer = new Array[Byte](65536) |
291 |
var c = -1 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
292 |
|
52799 | 293 |
def read_int(): Int = |
294 |
//{{{ |
|
34100 | 295 |
{ |
296 |
var n = 0 |
|
297 |
c = stream.read |
|
39526 | 298 |
if (c == -1) throw new EOF |
34100 | 299 |
while (48 <= c && c <= 57) { |
300 |
n = 10 * n + (c - 48) |
|
301 |
c = stream.read |
|
302 |
} |
|
52799 | 303 |
if (c != 10) |
304 |
throw new Protocol_Error("malformed header: expected integer followed by newline") |
|
305 |
else n |
|
306 |
} |
|
307 |
//}}} |
|
34100 | 308 |
|
52799 | 309 |
def read_chunk(do_decode: Boolean): XML.Body = |
310 |
//{{{ |
|
311 |
{ |
|
312 |
val n = read_int() |
|
34100 | 313 |
val buf = |
314 |
if (n <= default_buffer.size) default_buffer |
|
315 |
else new Array[Byte](n) |
|
316 |
||
317 |
var i = 0 |
|
318 |
var m = 0 |
|
319 |
do { |
|
320 |
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
|
321 |
if (m != -1) i += m |
52799 | 322 |
} |
323 |
while (m != -1 && n > i) |
|
34100 | 324 |
|
52799 | 325 |
if (i != n) |
326 |
throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)") |
|
34100 | 327 |
|
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
328 |
if (do_decode) |
50203 | 329 |
YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n)) |
330 |
else List(XML.Text(UTF8.decode_chars(s => s, buf, 0, n).toString)) |
|
34100 | 331 |
} |
52799 | 332 |
//}}} |
34100 | 333 |
|
46769 | 334 |
try { |
335 |
do { |
|
336 |
try { |
|
337 |
val header = read_chunk(true) |
|
338 |
header match { |
|
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49445
diff
changeset
|
339 |
case List(XML.Elem(Markup(name, props), Nil)) => |
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49445
diff
changeset
|
340 |
val kind = name.intern |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
341 |
val body = read_chunk(kind != Markup.PROTOCOL) |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
342 |
output_message(kind, props, body) |
46769 | 343 |
case _ => |
344 |
read_chunk(false) |
|
345 |
throw new Protocol_Error("bad header: " + header.toString) |
|
346 |
} |
|
28063 | 347 |
} |
46769 | 348 |
catch { case _: EOF => } |
52799 | 349 |
} |
350 |
while (c != -1) |
|
46769 | 351 |
} |
352 |
catch { |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
353 |
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
|
354 |
case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage) |
46769 | 355 |
} |
34100 | 356 |
stream.close |
357 |
||
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
358 |
system_output(name + " terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
359 |
} |
39526 | 360 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
361 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
362 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
363 |
/** main methods **/ |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
364 |
|
52582 | 365 |
def protocol_command_raw(name: String, args: Array[Byte]*): Unit = |
50203 | 366 |
command_input._2 ! Input_Chunks(UTF8.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
|
367 |
|
52582 | 368 |
def protocol_command(name: String, args: String*) |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
369 |
{ |
44732 | 370 |
receiver(new Input(name, args.toList)) |
52582 | 371 |
protocol_command_raw(name, args.map(UTF8.string_bytes): _*) |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
372 |
} |
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
373 |
|
50117 | 374 |
def options(opts: Options): Unit = |
52582 | 375 |
protocol_command("Isabelle_Process.options", YXML.string_of_body(opts.encode)) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
376 |
} |