author | wenzelm |
Sun, 04 Sep 2011 14:29:15 +0200 | |
changeset 44697 | b99dfee76538 |
parent 43780 | 2cb2310d68b6 |
child 44705 | 089fcaf94c00 |
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 |
{ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
21 |
/* results */ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
22 |
|
39525 | 23 |
object Kind |
24 |
{ |
|
25 |
val message_markup = Map( |
|
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
26 |
('A' : Int) -> Markup.INIT, |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
27 |
('B' : Int) -> Markup.STATUS, |
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
28 |
('C' : Int) -> Markup.REPORT, |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
29 |
('D' : Int) -> Markup.WRITELN, |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
30 |
('E' : Int) -> Markup.TRACING, |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
31 |
('F' : Int) -> Markup.WARNING, |
43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
32 |
('G' : Int) -> Markup.ERROR, |
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
33 |
('H' : Int) -> Markup.RAW) |
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 |
|
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
36 |
abstract class Message |
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 = |
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
41 |
XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))), |
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
42 |
args.map(s => |
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
43 |
List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString |
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
44 |
} |
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 |
class Result(val message: XML.Elem) extends Message |
34100 | 47 |
{ |
43747 | 48 |
def kind: String = message.markup.name |
43780 | 49 |
def properties: Properties.T = message.markup.properties |
43747 | 50 |
def body: XML.Body = message.body |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
51 |
|
39525 | 52 |
def is_init = kind == Markup.INIT |
53 |
def is_exit = kind == Markup.EXIT |
|
54 |
def is_stdout = kind == Markup.STDOUT |
|
55 |
def is_system = kind == Markup.SYSTEM |
|
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
56 |
def is_status = kind == Markup.STATUS |
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
57 |
def is_report = kind == Markup.REPORT |
43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
58 |
def is_raw = kind == Markup.RAW |
39625 | 59 |
def is_ready = Isar_Document.is_ready(message) |
60 |
def is_syslog = is_init || is_exit || is_system || is_ready |
|
34100 | 61 |
|
62 |
override def toString: String = |
|
63 |
{ |
|
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
64 |
val res = |
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
65 |
if (is_status || is_report) message.body.map(_.toString).mkString |
43748 | 66 |
else if (is_raw) "..." |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
67 |
else Pretty.string_of(message.body) |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37712
diff
changeset
|
68 |
if (properties.isEmpty) |
29572
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
69 |
kind.toString + " [[" + res + "]]" |
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
70 |
else |
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
71 |
kind.toString + " " + |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37712
diff
changeset
|
72 |
(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
|
73 |
} |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
74 |
} |
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 |
|
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43520
diff
changeset
|
78 |
class Isabelle_Process(timeout: Time, receiver: Actor, args: String*) |
29192 | 79 |
{ |
31797 | 80 |
import Isabelle_Process._ |
29194 | 81 |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
82 |
|
29192 | 83 |
/* demo constructor */ |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
84 |
|
29192 | 85 |
def this(args: String*) = |
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43520
diff
changeset
|
86 |
this(Time.seconds(10), actor { loop { react { case res => Console.println(res) } } }, args: _*) |
29174 | 87 |
|
88 |
||
39626
a5d0bcfb95a3
manage persistent syslog via Session, not Isabelle_Process;
wenzelm
parents:
39625
diff
changeset
|
89 |
/* results */ |
39573 | 90 |
|
91 |
private def system_result(text: String) |
|
92 |
{ |
|
93 |
receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text)))) |
|
94 |
} |
|
95 |
||
43745 | 96 |
private val xml_cache = new XML.Cache() |
39573 | 97 |
|
43780 | 98 |
private def put_result(kind: String, props: Properties.T, body: XML.Body) |
39573 | 99 |
{ |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
100 |
if (kind == Markup.INIT) rm_fifos() |
43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
101 |
if (kind == Markup.RAW) |
44697
b99dfee76538
pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
wenzelm
parents:
43780
diff
changeset
|
102 |
xml_cache.cache_ignore( |
b99dfee76538
pass raw messages through xml_cache actor, which is important to retain ordering of results (e.g. read_command reports before assign, cf. 383c9d758a56);
wenzelm
parents:
43780
diff
changeset
|
103 |
new Result(XML.Elem(Markup(kind, props), body)))((result: Result) => receiver ! result) |
43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
104 |
else { |
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
105 |
val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body)) |
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
106 |
xml_cache.cache_tree(msg)((message: XML.Tree) => |
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
107 |
receiver ! new Result(message.asInstanceOf[XML.Elem])) |
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
108 |
} |
39573 | 109 |
} |
110 |
||
111 |
private def put_result(kind: String, text: String) |
|
112 |
{ |
|
43695
5130dfe1b7be
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
wenzelm
parents:
43661
diff
changeset
|
113 |
put_result(kind, Nil, List(XML.Text(Symbol.decode(text)))) |
39573 | 114 |
} |
115 |
||
116 |
||
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
|
117 |
/* 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
|
118 |
|
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
119 |
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
|
120 |
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
|
121 |
|
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
122 |
private case object Close |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
123 |
private def close(p: (Thread, Actor)) |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
124 |
{ |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
125 |
if (p != null && p._1.isAlive) { |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
126 |
p._2 ! Close |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
127 |
p._1.join |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
128 |
} |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
129 |
} |
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
|
130 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
131 |
@volatile private var standard_input: (Thread, Actor) = null |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
132 |
@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
|
133 |
|
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
134 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
135 |
/** 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
|
136 |
|
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43520
diff
changeset
|
137 |
private val in_fifo = Isabelle_System.mk_fifo() |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43520
diff
changeset
|
138 |
private val out_fifo = Isabelle_System.mk_fifo() |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43520
diff
changeset
|
139 |
private def rm_fifos() { Isabelle_System.rm_fifo(in_fifo); Isabelle_System.rm_fifo(out_fifo) } |
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 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
141 |
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
|
142 |
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
|
143 |
val cmdline = |
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43520
diff
changeset
|
144 |
List(Isabelle_System.getenv_strict("ISABELLE_PROCESS"), "-W", |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43520
diff
changeset
|
145 |
in_fifo + ":" + out_fifo) ++ args |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43520
diff
changeset
|
146 |
new Isabelle_System.Managed_Process(true, cmdline: _*) |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
147 |
} |
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 |
catch { case e: IOException => rm_fifos(); throw(e) } |
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
149 |
|
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
150 |
val process_result = |
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
151 |
Simple_Thread.future("process_result") { process.join } |
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
152 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
153 |
private def terminate_process() |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
154 |
{ |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
155 |
try { process.terminate } |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
156 |
catch { case e: IOException => system_result("Failed to terminate Isabelle: " + e.getMessage) } |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
157 |
} |
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
|
158 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
159 |
private val process_manager = Simple_Thread.fork("process_manager") |
39572 | 160 |
{ |
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
|
161 |
val (startup_failed, startup_output) = |
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
162 |
{ |
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
39731
diff
changeset
|
163 |
val expired = System.currentTimeMillis() + timeout.ms |
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 |
val result = new StringBuilder(100) |
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
165 |
|
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
166 |
var finished: Option[Boolean] = None |
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
167 |
while (finished.isEmpty && System.currentTimeMillis() <= expired) { |
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
168 |
while (finished.isEmpty && process.stdout.ready) { |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
169 |
val c = process.stdout.read |
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
170 |
if (c == 2) finished = Some(true) |
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
|
171 |
else result += c.toChar |
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
172 |
} |
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
173 |
if (process_result.is_finished) finished = Some(false) |
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
174 |
else 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
|
175 |
} |
39623 | 176 |
(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
|
177 |
} |
39572 | 178 |
system_result(startup_output) |
179 |
||
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 |
if (startup_failed) { |
39632 | 181 |
put_result(Markup.EXIT, "Return code: 127") |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
182 |
process.stdin.close |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
183 |
Thread.sleep(300) |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
184 |
terminate_process() |
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
185 |
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
|
186 |
} |
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
187 |
else { |
39530
16adc476348f
Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents:
39528
diff
changeset
|
188 |
// rendezvous |
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43520
diff
changeset
|
189 |
val command_stream = Isabelle_System.fifo_output_stream(in_fifo) |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43520
diff
changeset
|
190 |
val message_stream = Isabelle_System.fifo_input_stream(out_fifo) |
39530
16adc476348f
Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents:
39528
diff
changeset
|
191 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
192 |
standard_input = stdin_actor() |
39572 | 193 |
val stdout = stdout_actor() |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
194 |
command_input = input_actor(command_stream) |
39572 | 195 |
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
|
196 |
|
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
197 |
val rc = process_result.join |
39618 | 198 |
system_result("process terminated") |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
199 |
for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join |
39572 | 200 |
system_result("process_manager terminated") |
39632 | 201 |
put_result(Markup.EXIT, "Return code: " + rc.toString) |
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
|
202 |
} |
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
203 |
rm_fifos() |
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
204 |
} |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
205 |
|
39572 | 206 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
207 |
/* management methods */ |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
208 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
209 |
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
|
210 |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
211 |
def interrupt() |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
212 |
{ |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
213 |
try { process.interrupt } |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
214 |
catch { case e: IOException => system_result("Failed to interrupt Isabelle: " + e.getMessage) } |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
215 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
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 |
{ |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
219 |
close() |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
220 |
system_result("Terminating Isabelle process") |
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 |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
228 |
/* raw stdin */ |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
229 |
|
39572 | 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) { |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
234 |
var finished = false |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
235 |
while (!finished) { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
236 |
try { |
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 |
} |
39525 | 249 |
catch { case e: IOException => system_result(name + ": " + e.getMessage) } |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
250 |
} |
39525 | 251 |
system_result(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 |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
256 |
/* raw stdout */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
257 |
|
39572 | 258 |
private def stdout_actor(): (Thread, Actor) = |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
259 |
{ |
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
|
260 |
val name = "standard_output" |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
38573
diff
changeset
|
261 |
Simple_Thread.actor(name) { |
28045 | 262 |
var result = new StringBuilder(100) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
263 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
264 |
var finished = false |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
265 |
while (!finished) { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
266 |
try { |
28045 | 267 |
//{{{ |
268 |
var c = -1 |
|
269 |
var done = false |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
270 |
while (!done && (result.length == 0 || process.stdout.ready)) { |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
271 |
c = process.stdout.read |
28045 | 272 |
if (c >= 0) result.append(c.asInstanceOf[Char]) |
273 |
else done = true |
|
274 |
} |
|
275 |
if (result.length > 0) { |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
276 |
put_result(Markup.STDOUT, result.toString) |
28045 | 277 |
result.length = 0 |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
278 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
279 |
else { |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
280 |
process.stdout.close |
28045 | 281 |
finished = true |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
282 |
} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
283 |
//}}} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
284 |
} |
39525 | 285 |
catch { case e: IOException => system_result(name + ": " + e.getMessage) } |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
286 |
} |
39525 | 287 |
system_result(name + " terminated") |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
288 |
} |
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
|
289 |
} |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
290 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
291 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
292 |
/* command input */ |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
293 |
|
39572 | 294 |
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
|
295 |
{ |
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
|
296 |
val name = "command_input" |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
38573
diff
changeset
|
297 |
Simple_Thread.actor(name) { |
39530
16adc476348f
Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents:
39528
diff
changeset
|
298 |
val stream = new BufferedOutputStream(raw_stream) |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
299 |
var finished = false |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
300 |
while (!finished) { |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
301 |
try { |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
302 |
//{{{ |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
303 |
receive { |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
304 |
case Input_Chunks(chunks) => |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
305 |
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
|
306 |
chunks.map(_.length).mkString("", ",", "\n"))); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
307 |
chunks.foreach(stream.write(_)); |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
308 |
stream.flush |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
309 |
case Close => |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
310 |
stream.close |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
311 |
finished = true |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
312 |
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
|
313 |
} |
28045 | 314 |
//}}} |
27963 | 315 |
} |
39525 | 316 |
catch { case e: IOException => system_result(name + ": " + e.getMessage) } |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
317 |
} |
39525 | 318 |
system_result(name + " terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
319 |
} |
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
|
320 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
321 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
322 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
323 |
/* message output */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
324 |
|
39572 | 325 |
private def message_actor(stream: InputStream): (Thread, Actor) = |
39526 | 326 |
{ |
327 |
class EOF extends Exception |
|
328 |
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
|
329 |
|
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
|
330 |
val name = "message_output" |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
38573
diff
changeset
|
331 |
Simple_Thread.actor(name) { |
34100 | 332 |
val default_buffer = new Array[Byte](65536) |
333 |
var c = -1 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
334 |
|
43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
335 |
def read_chunk(decode: Boolean): XML.Body = |
34100 | 336 |
{ |
337 |
//{{{ |
|
338 |
// chunk size |
|
339 |
var n = 0 |
|
340 |
c = stream.read |
|
39526 | 341 |
if (c == -1) throw new EOF |
34100 | 342 |
while (48 <= c && c <= 57) { |
343 |
n = 10 * n + (c - 48) |
|
344 |
c = stream.read |
|
345 |
} |
|
346 |
if (c != 10) throw new Protocol_Error("bad message chunk header") |
|
347 |
||
348 |
// chunk content |
|
349 |
val buf = |
|
350 |
if (n <= default_buffer.size) default_buffer |
|
351 |
else new Array[Byte](n) |
|
352 |
||
353 |
var i = 0 |
|
354 |
var m = 0 |
|
355 |
do { |
|
356 |
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
|
357 |
if (m != -1) i += m |
5cb0d7b0d601
bulk read: observe EOF protocol more carefully -- 0 counts as successful read;
wenzelm
parents:
39632
diff
changeset
|
358 |
} while (m != -1 && n > i) |
34100 | 359 |
|
360 |
if (i != n) throw new Protocol_Error("bad message chunk content") |
|
361 |
||
43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
362 |
if (decode) |
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
363 |
YXML.parse_body_failsafe(Standard_System.decode_chars(Symbol.decode, buf, 0, n)) |
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
364 |
else List(XML.Text(Standard_System.decode_chars(s => s, buf, 0, n).toString)) |
34100 | 365 |
//}}} |
366 |
} |
|
367 |
||
368 |
do { |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
369 |
try { |
43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
370 |
val header = read_chunk(true) |
38445
ba9ea6b9b75c
simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents:
38372
diff
changeset
|
371 |
header match { |
ba9ea6b9b75c
simplified internal message format: dropped special Symbol.STX header;
wenzelm
parents:
38372
diff
changeset
|
372 |
case List(XML.Elem(Markup(name, props), Nil)) |
39525 | 373 |
if name.size == 1 && Kind.message_markup.isDefinedAt(name(0)) => |
43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
374 |
val kind = Kind.message_markup(name(0)) |
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
375 |
val body = read_chunk(kind != Markup.RAW) |
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
376 |
put_result(kind, props, body) |
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
377 |
case _ => |
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
378 |
read_chunk(false) |
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43745
diff
changeset
|
379 |
throw new Protocol_Error("bad header: " + header.toString) |
28063 | 380 |
} |
27963 | 381 |
} |
28063 | 382 |
catch { |
39525 | 383 |
case e: IOException => system_result("Cannot read message:\n" + e.getMessage) |
384 |
case e: Protocol_Error => system_result("Malformed message:\n" + e.getMessage) |
|
39526 | 385 |
case _: EOF => |
28063 | 386 |
} |
34100 | 387 |
} while (c != -1) |
388 |
stream.close |
|
389 |
||
39525 | 390 |
system_result(name + " terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
391 |
} |
39526 | 392 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
393 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
394 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
395 |
/** main methods **/ |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
396 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
397 |
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
|
398 |
|
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
|
399 |
def input_bytes(name: String, args: Array[Byte]*): Unit = |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
400 |
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
|
401 |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
402 |
def input(name: String, args: String*): Unit = |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
403 |
{ |
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
404 |
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
|
405 |
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
|
406 |
} |
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
407 |
|
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
|
408 |
def close(): Unit = { close(command_input); close(standard_input) } |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
409 |
} |