author | wenzelm |
Tue, 10 Aug 2010 15:12:45 +0200 | |
changeset 38262 | bb2df73fab2c |
parent 38259 | 2b61c5e27399 |
child 38270 | 71bb3c273dd1 |
permissions | -rw-r--r-- |
30173
eabece26b89b
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents:
29648
diff
changeset
|
1 |
/* Title: Pure/System/isabelle_process.ML |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
27963 | 3 |
Options: :folding=explicit:collapseFolds=1: |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
4 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
5 |
Isabelle process management -- always reactive due to multi-threaded I/O. |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
6 |
*/ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
7 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
8 |
package isabelle |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
9 |
|
27955
4c32c5e75eca
use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
wenzelm
parents:
27949
diff
changeset
|
10 |
import java.util.concurrent.LinkedBlockingQueue |
28045 | 11 |
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, |
28056 | 12 |
InputStream, OutputStream, IOException} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
13 |
|
32474
0818e6b1c8a6
Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents:
32448
diff
changeset
|
14 |
import scala.actors.Actor |
0818e6b1c8a6
Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents:
32448
diff
changeset
|
15 |
import Actor._ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
16 |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
17 |
|
32474
0818e6b1c8a6
Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents:
32448
diff
changeset
|
18 |
object Isabelle_Process |
0818e6b1c8a6
Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents:
32448
diff
changeset
|
19 |
{ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
20 |
/* results */ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
21 |
|
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
22 |
object Kind { |
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
23 |
// message markup |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
24 |
val markup = Map( |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
25 |
('A' : Int) -> Markup.INIT, |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
26 |
('B' : Int) -> Markup.STATUS, |
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
27 |
('C' : Int) -> Markup.REPORT, |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
28 |
('D' : Int) -> Markup.WRITELN, |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
29 |
('E' : Int) -> Markup.TRACING, |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
30 |
('F' : Int) -> Markup.WARNING, |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
31 |
('G' : Int) -> Markup.ERROR, |
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
32 |
('H' : Int) -> Markup.DEBUG) |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
33 |
def is_raw(kind: String) = |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
34 |
kind == Markup.STDOUT |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
35 |
def is_control(kind: String) = |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
36 |
kind == Markup.SYSTEM || |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
37 |
kind == Markup.SIGNAL || |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
38 |
kind == Markup.EXIT |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
39 |
def is_system(kind: String) = |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
40 |
kind == Markup.SYSTEM || |
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
41 |
kind == Markup.INPUT || |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
42 |
kind == Markup.STDIN || |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
43 |
kind == Markup.SIGNAL || |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
44 |
kind == Markup.EXIT || |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
45 |
kind == Markup.STATUS |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
46 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
47 |
|
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
48 |
class Result(val message: XML.Elem) |
34100 | 49 |
{ |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37712
diff
changeset
|
50 |
def kind = message.markup.name |
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37712
diff
changeset
|
51 |
def properties = message.markup.properties |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
52 |
def body = message.body |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
53 |
|
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
54 |
def is_raw = Kind.is_raw(kind) |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
55 |
def is_control = Kind.is_control(kind) |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
56 |
def is_system = Kind.is_system(kind) |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
57 |
def is_status = kind == Markup.STATUS |
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
58 |
def is_report = kind == Markup.REPORT |
38231 | 59 |
def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil)) |
34100 | 60 |
|
61 |
override def toString: String = |
|
62 |
{ |
|
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
63 |
val res = |
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
64 |
if (is_status || is_report) message.body.map(_.toString).mkString |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
65 |
else Pretty.string_of(message.body) |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37712
diff
changeset
|
66 |
if (properties.isEmpty) |
29572
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
67 |
kind.toString + " [[" + res + "]]" |
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
68 |
else |
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
69 |
kind.toString + " " + |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37712
diff
changeset
|
70 |
(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
|
71 |
} |
34109 | 72 |
|
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
73 |
def cache(c: XML.Cache): Result = new Result(c.cache_tree(message).asInstanceOf[XML.Elem]) |
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 |
|
34100 | 78 |
class Isabelle_Process(system: Isabelle_System, 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*) = |
32474
0818e6b1c8a6
Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents:
32448
diff
changeset
|
86 |
this(new Isabelle_System, |
34213
9e86c1ca6e51
removed obsolete version check -- sanity delegated to Isabelle_System;
wenzelm
parents:
34201
diff
changeset
|
87 |
actor { loop { react { case res => Console.println(res) } } }, args: _*) |
29174 | 88 |
|
89 |
||
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
90 |
/* process information */ |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
91 |
|
29648 | 92 |
@volatile private var proc: Process = null |
93 |
@volatile private var closing = false |
|
94 |
@volatile private var pid: String = null |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
95 |
|
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
96 |
|
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
97 |
/* results */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
98 |
|
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
99 |
private def put_result(kind: String, props: List[(String, String)], body: List[XML.Tree]) |
29572
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
100 |
{ |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
101 |
if (kind == Markup.INIT) { |
34214
99eefb83a35d
simplified init message -- removed redundant session property;
wenzelm
parents:
34213
diff
changeset
|
102 |
for ((Markup.PID, p) <- props) pid = p |
27963 | 103 |
} |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37712
diff
changeset
|
104 |
receiver ! new Result(XML.Elem(Markup(kind, props), body)) |
34100 | 105 |
} |
106 |
||
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
107 |
private def put_result(kind: String, text: String) |
34100 | 108 |
{ |
109 |
put_result(kind, Nil, List(XML.Text(system.symbols.decode(text)))) |
|
27992 | 110 |
} |
111 |
||
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
112 |
|
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
113 |
/* signals */ |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
114 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
115 |
def interrupt() = synchronized { // FIXME avoid synchronized |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
116 |
if (proc == null) error("Cannot interrupt Isabelle: no process") |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
117 |
if (pid == null) put_result(Markup.SYSTEM, "Cannot interrupt: unknown pid") |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
118 |
else { |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
119 |
try { |
34100 | 120 |
if (system.execute(true, "kill", "-INT", pid).waitFor == 0) |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
121 |
put_result(Markup.SIGNAL, "INT") |
27990 | 122 |
else |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
123 |
put_result(Markup.SYSTEM, "Cannot interrupt: kill command failed") |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
124 |
} |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
125 |
catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) } |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
126 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
127 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
128 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
129 |
def kill() = synchronized { // FIXME avoid synchronized |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
130 |
if (proc == 0) error("Cannot kill Isabelle: no process") |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
131 |
else { |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
132 |
try_close() |
37132 | 133 |
Thread.sleep(500) // FIXME property!? |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
134 |
put_result(Markup.SIGNAL, "KILL") |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
135 |
proc.destroy |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
136 |
proc = null |
27990 | 137 |
pid = null |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
138 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
139 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
140 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
141 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
142 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
143 |
/** stream actors **/ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
144 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
145 |
/* input */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
146 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
147 |
case class Input(cmd: String) |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
148 |
case object Close |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
149 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
150 |
private def input_actor(name: String, kind: String, stream: => OutputStream): Actor = |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
151 |
Library.thread_actor(name) { |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
152 |
val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset)) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
153 |
var finished = false |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
154 |
while (!finished) { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
155 |
try { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
156 |
//{{{ |
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
157 |
receive { |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
158 |
case Input(text) => |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
159 |
put_result(kind, text) |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
160 |
writer.write(text) |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
161 |
writer.flush |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
162 |
case Close => |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
163 |
writer.close |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
164 |
finished = true |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
165 |
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
|
166 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
167 |
//}}} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
168 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
169 |
catch { |
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
170 |
case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
171 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
172 |
} |
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
173 |
put_result(Markup.SYSTEM, name + " terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
174 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
175 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
176 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
177 |
/* raw output */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
178 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
179 |
private def output_actor(name: String, kind: String, stream: => InputStream): Actor = |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
180 |
Library.thread_actor(name) { |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
181 |
val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset)) |
28045 | 182 |
var result = new StringBuilder(100) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
183 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
184 |
var finished = false |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
185 |
while (!finished) { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
186 |
try { |
28045 | 187 |
//{{{ |
188 |
var c = -1 |
|
189 |
var done = false |
|
190 |
while (!done && (result.length == 0 || reader.ready)) { |
|
191 |
c = reader.read |
|
192 |
if (c >= 0) result.append(c.asInstanceOf[Char]) |
|
193 |
else done = true |
|
194 |
} |
|
195 |
if (result.length > 0) { |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
196 |
put_result(kind, result.toString) |
28045 | 197 |
result.length = 0 |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
198 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
199 |
else { |
28045 | 200 |
reader.close |
201 |
finished = true |
|
202 |
try_close() |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
203 |
} |
28045 | 204 |
//}}} |
27963 | 205 |
} |
206 |
catch { |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
207 |
case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
208 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
209 |
} |
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
210 |
put_result(Markup.SYSTEM, name + " terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
211 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
212 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
213 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
214 |
/* message output */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
215 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
216 |
private class Protocol_Error(msg: String) extends Exception(msg) |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
217 |
|
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
218 |
private def message_actor(name: String, stream: InputStream): Actor = |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
219 |
Library.thread_actor(name) { |
34100 | 220 |
val default_buffer = new Array[Byte](65536) |
221 |
var c = -1 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
222 |
|
34100 | 223 |
def read_chunk(): List[XML.Tree] = |
224 |
{ |
|
225 |
//{{{ |
|
226 |
// chunk size |
|
227 |
var n = 0 |
|
228 |
c = stream.read |
|
229 |
while (48 <= c && c <= 57) { |
|
230 |
n = 10 * n + (c - 48) |
|
231 |
c = stream.read |
|
232 |
} |
|
233 |
if (c != 10) throw new Protocol_Error("bad message chunk header") |
|
234 |
||
235 |
// chunk content |
|
236 |
val buf = |
|
237 |
if (n <= default_buffer.size) default_buffer |
|
238 |
else new Array[Byte](n) |
|
239 |
||
240 |
var i = 0 |
|
241 |
var m = 0 |
|
242 |
do { |
|
243 |
m = stream.read(buf, i, n - i) |
|
244 |
i += m |
|
245 |
} while (m > 0 && n > i) |
|
246 |
||
247 |
if (i != n) throw new Protocol_Error("bad message chunk content") |
|
248 |
||
249 |
YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n)) |
|
250 |
//}}} |
|
251 |
} |
|
252 |
||
253 |
do { |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
254 |
try { |
34100 | 255 |
//{{{ |
256 |
c = stream.read |
|
257 |
var non_sync = 0 |
|
258 |
while (c >= 0 && c != 2) { |
|
259 |
non_sync += 1 |
|
260 |
c = stream.read |
|
28063 | 261 |
} |
34100 | 262 |
if (non_sync > 0) |
263 |
throw new Protocol_Error("lost synchronization -- skipping " + non_sync + " bytes") |
|
264 |
if (c == 2) { |
|
265 |
val header = read_chunk() |
|
266 |
val body = read_chunk() |
|
267 |
header match { |
|
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37712
diff
changeset
|
268 |
case List(XML.Elem(Markup(name, props), Nil)) |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
269 |
if name.size == 1 && Kind.markup.isDefinedAt(name(0)) => |
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
270 |
put_result(Kind.markup(name(0)), props, body) |
34100 | 271 |
case _ => throw new Protocol_Error("bad header: " + header.toString) |
28063 | 272 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
273 |
} |
34100 | 274 |
//}}} |
27963 | 275 |
} |
28063 | 276 |
catch { |
34100 | 277 |
case e: IOException => |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
278 |
put_result(Markup.SYSTEM, "Cannot read message:\n" + e.getMessage) |
34100 | 279 |
case e: Protocol_Error => |
37689
628eabe2213a
simplified Isabelle_Process.Result: use markup directly;
wenzelm
parents:
37132
diff
changeset
|
280 |
put_result(Markup.SYSTEM, "Malformed message:\n" + e.getMessage) |
28063 | 281 |
} |
34100 | 282 |
} while (c != -1) |
283 |
stream.close |
|
284 |
try_close() |
|
285 |
||
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
286 |
put_result(Markup.SYSTEM, name + " terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
287 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
288 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
289 |
|
29192 | 290 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
291 |
/** init **/ |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
292 |
|
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
293 |
/* exec process */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
294 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
295 |
private val in_fifo = system.mk_fifo() |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
296 |
private val out_fifo = system.mk_fifo() |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
297 |
private def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) } |
28045 | 298 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
299 |
try { |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
300 |
val cmdline = |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
301 |
List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
302 |
proc = system.execute(true, cmdline: _*) |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
303 |
} |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
304 |
catch { |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
305 |
case e: IOException => |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
306 |
rm_fifos() |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
307 |
error("Failed to execute Isabelle process: " + e.getMessage) |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
308 |
} |
28045 | 309 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
310 |
|
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
311 |
/* exit process */ |
38253
3d4e521014f7
Isabelle_Process: separate input fifo for commands (still using the old tty protocol);
wenzelm
parents:
38236
diff
changeset
|
312 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
313 |
Library.thread_actor("process_exit") { |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
314 |
val rc = proc.waitFor() |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
315 |
Thread.sleep(300) // FIXME property!? |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
316 |
put_result(Markup.SYSTEM, "process_exit terminated") |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
317 |
put_result(Markup.EXIT, rc.toString) |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
318 |
rm_fifos() |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
319 |
} |
28045 | 320 |
|
321 |
||
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
322 |
/* I/O actors */ |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
323 |
|
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
324 |
private val standard_input = |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
325 |
input_actor("standard_input", Markup.STDIN, proc.getOutputStream) |
27963 | 326 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
327 |
private val command_input = |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
328 |
input_actor("command_input", Markup.INPUT, system.fifo_output_stream(in_fifo)) |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
329 |
|
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
330 |
output_actor("standard_output", Markup.STDOUT, proc.getInputStream) |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
331 |
message_actor("message_output", system.fifo_input_stream(out_fifo)) |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
332 |
|
28045 | 333 |
|
334 |
||
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
335 |
/** main methods **/ |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
336 |
|
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
337 |
def input_raw(text: String) = standard_input ! Input(text) |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
338 |
|
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
339 |
def input(text: String) = synchronized { // FIXME avoid synchronized |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
340 |
if (proc == null) error("Cannot output to Isabelle: no process") |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
341 |
if (closing) error("Cannot output to Isabelle: already closing") |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
342 |
command_input ! Input(" \\<^sync>\n; " + text + " \\<^sync>;\n") |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
343 |
} |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
344 |
|
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
345 |
def close() = synchronized { // FIXME avoid synchronized |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
346 |
command_input ! Close |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
347 |
closing = true |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
348 |
} |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
349 |
|
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
350 |
def try_close() = synchronized { |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
351 |
if (proc != null && !closing) { |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
352 |
try { close() } |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
353 |
catch { case _: RuntimeException => } |
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
354 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
355 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
356 |
} |