author | wenzelm |
Mon, 29 Dec 2008 15:16:01 +0100 | |
changeset 29192 | 082ee2a01a6d |
parent 29178 | d41ccf3efbfc |
child 29194 | 53930d089f88 |
permissions | -rw-r--r-- |
27963 | 1 |
/* Title: Pure/Tools/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 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
10 |
import java.util.Properties |
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, |
28056 | 13 |
InputStream, OutputStream, IOException} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
14 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
15 |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
16 |
object IsabelleProcess { |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
17 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
18 |
/* results */ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
19 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
20 |
object Kind extends Enumeration { |
28344
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
21 |
//{{{ values and codes |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
22 |
// internal system notification |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
23 |
val SYSTEM = Value("SYSTEM") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
24 |
// Posix channels/events |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
25 |
val STDIN = Value("STDIN") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
26 |
val STDOUT = Value("STDOUT") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
27 |
val SIGNAL = Value("SIGNAL") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
28 |
val EXIT = Value("EXIT") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
29 |
// Isabelle messages |
28344
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
30 |
val INIT = Value("INIT") |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
31 |
val STATUS = Value("STATUS") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
32 |
val WRITELN = Value("WRITELN") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
33 |
val PRIORITY = Value("PRIORITY") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
34 |
val TRACING = Value("TRACING") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
35 |
val WARNING = Value("WARNING") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
36 |
val ERROR = Value("ERROR") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
37 |
val DEBUG = Value("DEBUG") |
28344
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
38 |
// messages codes |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
39 |
val code = Map( |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
40 |
('A' : Int) -> Kind.INIT, |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
41 |
('B' : Int) -> Kind.STATUS, |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
42 |
('C' : Int) -> Kind.WRITELN, |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
43 |
('D' : Int) -> Kind.PRIORITY, |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
44 |
('E' : Int) -> Kind.TRACING, |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
45 |
('F' : Int) -> Kind.WARNING, |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
46 |
('G' : Int) -> Kind.ERROR, |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
47 |
('H' : Int) -> Kind.DEBUG, |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
48 |
('0' : Int) -> Kind.SYSTEM, |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
49 |
('1' : Int) -> Kind.STDIN, |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
50 |
('2' : Int) -> Kind.STDOUT, |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
51 |
('3' : Int) -> Kind.SIGNAL, |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
52 |
('4' : Int) -> Kind.EXIT) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
53 |
//}}} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
54 |
def is_raw(kind: Value) = |
28045 | 55 |
kind == STDOUT |
27990 | 56 |
def is_control(kind: Value) = |
28344
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
57 |
kind == SYSTEM || |
27990 | 58 |
kind == SIGNAL || |
28344
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
59 |
kind == EXIT |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
60 |
def is_system(kind: Value) = |
28344
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
61 |
kind == SYSTEM || |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
62 |
kind == STDIN || |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
63 |
kind == SIGNAL || |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
64 |
kind == EXIT || |
28498 | 65 |
kind == STATUS |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
66 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
67 |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
68 |
class Result(val kind: Kind.Value, val props: Properties, val result: String) { |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
69 |
override def toString = { |
29174 | 70 |
val res = XML.content(YXML.parse_failsafe(result)).mkString |
27955
4c32c5e75eca
use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
wenzelm
parents:
27949
diff
changeset
|
71 |
if (props == null) kind.toString + " [[" + res + "]]" |
4c32c5e75eca
use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
wenzelm
parents:
27949
diff
changeset
|
72 |
else kind.toString + " " + props.toString + " [[" + res + "]]" |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
73 |
} |
29192 | 74 |
def is_raw = Kind.is_raw(kind) |
75 |
def is_control = Kind.is_control(kind) |
|
76 |
def is_system = Kind.is_system(kind) |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
77 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
78 |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
79 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
80 |
|
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
81 |
|
29192 | 82 |
class IsabelleProcess(isabelle_system: IsabelleSystem, |
83 |
results: EventBus[IsabelleProcess.Result], args: String*) |
|
84 |
{ |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
85 |
import IsabelleProcess._ |
29192 | 86 |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
87 |
|
29192 | 88 |
/* demo constructor */ |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
89 |
|
29192 | 90 |
def this(args: String*) = |
91 |
this(new IsabelleSystem, new EventBus[IsabelleProcess.Result] + (Console.println(_)), args: _*) |
|
29174 | 92 |
|
93 |
||
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
94 |
/* process information */ |
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 |
private var proc: Process = null |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
97 |
private var closing = false |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
98 |
private var pid: String = null |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
99 |
private var the_session: String = null |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
100 |
def session() = the_session |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
101 |
|
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
102 |
|
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
103 |
/* results */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
104 |
|
29192 | 105 |
private val result_queue = new LinkedBlockingQueue[Result] |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
106 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
107 |
private def put_result(kind: Kind.Value, props: Properties, result: String) { |
27963 | 108 |
if (kind == Kind.INIT && props != null) { |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
109 |
pid = props.getProperty(Markup.PID) |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
110 |
the_session = props.getProperty(Markup.SESSION) |
27963 | 111 |
} |
29192 | 112 |
result_queue.put(new Result(kind, props, result)) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
113 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
114 |
|
29192 | 115 |
private class ResultThread extends Thread("isabelle: results") { |
116 |
override def run() = { |
|
117 |
var finished = false |
|
118 |
while (!finished) { |
|
119 |
val result = |
|
120 |
try { result_queue.take } |
|
121 |
catch { case _: NullPointerException => null } |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
122 |
|
29192 | 123 |
if (result != null) { |
124 |
results.event(result) // FIXME try/catch (!??) |
|
125 |
if (result.kind == Kind.EXIT) finished = true |
|
126 |
} |
|
127 |
else finished = true |
|
128 |
} |
|
129 |
} |
|
27992 | 130 |
} |
131 |
||
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
132 |
|
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
133 |
/* signals */ |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
134 |
|
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
135 |
def interrupt() = synchronized { |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
136 |
if (proc == null) error("Cannot interrupt Isabelle: no process") |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
137 |
if (pid == null) put_result(Kind.SYSTEM, null, "Cannot interrupt: unknown pid") |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
138 |
else { |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
139 |
try { |
29178 | 140 |
if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0) |
27990 | 141 |
put_result(Kind.SIGNAL, null, "INT") |
142 |
else |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
143 |
put_result(Kind.SYSTEM, null, "Cannot interrupt: kill command failed") |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
144 |
} |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
145 |
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
|
146 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
147 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
148 |
|
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
149 |
def kill() = synchronized { |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
150 |
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
|
151 |
else { |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
152 |
try_close() |
27990 | 153 |
Thread.sleep(500) |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
154 |
put_result(Kind.SIGNAL, null, "KILL") |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
155 |
proc.destroy |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
156 |
proc = null |
27990 | 157 |
pid = null |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
158 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
159 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
160 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
161 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
162 |
/* output being piped into the process */ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
163 |
|
27990 | 164 |
private val output = new LinkedBlockingQueue[String] |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
165 |
|
28045 | 166 |
private def output_raw(text: String) = synchronized { |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
167 |
if (proc == null) error("Cannot output to Isabelle: no process") |
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
168 |
if (closing) error("Cannot output to Isabelle: already closing") |
27955
4c32c5e75eca
use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
wenzelm
parents:
27949
diff
changeset
|
169 |
output.put(text) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
170 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
171 |
|
28303 | 172 |
def output_sync(text: String) = |
28045 | 173 |
output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
174 |
|
27963 | 175 |
|
176 |
def command(text: String) = |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
177 |
output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text)) |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
178 |
|
27963 | 179 |
def command(props: Properties, text: String) = |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
180 |
output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " + |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
181 |
IsabelleSyntax.encode_string(text)) |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
182 |
|
27963 | 183 |
def ML(text: String) = |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
184 |
output_sync("ML_val " + IsabelleSyntax.encode_string(text)) |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
185 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
186 |
def close() = synchronized { // FIXME watchdog/timeout |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
187 |
output_raw("\u0000") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
188 |
closing = true |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
189 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
190 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
191 |
def try_close() = synchronized { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
192 |
if (proc != null && !closing) { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
193 |
try { close() } |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
194 |
catch { case _: RuntimeException => } |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
195 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
196 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
197 |
|
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 |
/* stdin */ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
200 |
|
28045 | 201 |
private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") { |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
202 |
override def run() = { |
29174 | 203 |
val writer = new BufferedWriter(new OutputStreamWriter(out_stream, isabelle_system.charset)) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
204 |
var finished = false |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
205 |
while (!finished) { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
206 |
try { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
207 |
//{{{ |
27955
4c32c5e75eca
use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
wenzelm
parents:
27949
diff
changeset
|
208 |
val s = output.take |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
209 |
if (s == "\u0000") { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
210 |
writer.close |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
211 |
finished = true |
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 |
else { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
214 |
put_result(Kind.STDIN, null, s) |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
215 |
writer.write(s) |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
216 |
writer.flush |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
217 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
218 |
//}}} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
219 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
220 |
catch { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
221 |
case e: IOException => put_result(Kind.SYSTEM, null, "Stdin thread: " + e.getMessage) |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
222 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
223 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
224 |
put_result(Kind.SYSTEM, null, "Stdin thread terminated") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
225 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
226 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
227 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
228 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
229 |
/* stdout */ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
230 |
|
28045 | 231 |
private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") { |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
232 |
override def run() = { |
29174 | 233 |
val reader = new BufferedReader(new InputStreamReader(in_stream, isabelle_system.charset)) |
28045 | 234 |
var result = new StringBuilder(100) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
235 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
236 |
var finished = false |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
237 |
while (!finished) { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
238 |
try { |
28045 | 239 |
//{{{ |
240 |
var c = -1 |
|
241 |
var done = false |
|
242 |
while (!done && (result.length == 0 || reader.ready)) { |
|
243 |
c = reader.read |
|
244 |
if (c >= 0) result.append(c.asInstanceOf[Char]) |
|
245 |
else done = true |
|
246 |
} |
|
247 |
if (result.length > 0) { |
|
248 |
put_result(Kind.STDOUT, null, result.toString) |
|
249 |
result.length = 0 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
250 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
251 |
else { |
28045 | 252 |
reader.close |
253 |
finished = true |
|
254 |
try_close() |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
255 |
} |
28045 | 256 |
//}}} |
27963 | 257 |
} |
258 |
catch { |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
259 |
case e: IOException => put_result(Kind.SYSTEM, null, "Stdout thread: " + e.getMessage) |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
260 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
261 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
262 |
put_result(Kind.SYSTEM, null, "Stdout thread terminated") |
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 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
265 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
266 |
|
28045 | 267 |
/* messages */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
268 |
|
28045 | 269 |
private class MessageThread(fifo: String) extends Thread("isabelle: messages") { |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
270 |
override def run() = { |
29174 | 271 |
val reader = isabelle_system.fifo_reader(fifo) |
28045 | 272 |
var kind: Kind.Value = null |
273 |
var props: Properties = null |
|
274 |
var result = new StringBuilder |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
275 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
276 |
var finished = false |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
277 |
while (!finished) { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
278 |
try { |
28063 | 279 |
if (kind == null) { |
280 |
//{{{ Char mode -- resync |
|
281 |
var c = -1 |
|
282 |
do { |
|
283 |
c = reader.read |
|
284 |
if (c >= 0 && c != 2) result.append(c.asInstanceOf[Char]) |
|
285 |
} while (c >= 0 && c != 2) |
|
286 |
||
287 |
if (result.length > 0) { |
|
288 |
put_result(Kind.SYSTEM, null, "Malformed message:\n" + result.toString) |
|
289 |
result.length = 0 |
|
290 |
} |
|
291 |
if (c < 0) { |
|
292 |
reader.close |
|
293 |
finished = true |
|
294 |
try_close() |
|
28045 | 295 |
} |
296 |
else { |
|
28344
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
297 |
c = reader.read |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
298 |
if (Kind.code.isDefinedAt(c)) kind = Kind.code(c) |
f4a17868bde5
protocol change: remapped message codes to make room for nested system messages (e.g. for protocol proxy);
wenzelm
parents:
28303
diff
changeset
|
299 |
else kind = null |
28063 | 300 |
props = null |
301 |
} |
|
302 |
//}}} |
|
303 |
} |
|
304 |
else { |
|
305 |
//{{{ Line mode |
|
306 |
val line = reader.readLine |
|
307 |
if (line == null) { |
|
308 |
reader.close |
|
309 |
finished = true |
|
310 |
try_close() |
|
311 |
} |
|
312 |
else { |
|
313 |
val len = line.length |
|
314 |
// property |
|
315 |
if (line.endsWith("\u0002,")) { |
|
316 |
val i = line.indexOf('=') |
|
317 |
if (i > 0) { |
|
318 |
val name = line.substring(0, i) |
|
319 |
val value = line.substring(i + 1, len - 2) |
|
320 |
if (props == null) props = new Properties |
|
321 |
if (!props.containsKey(name)) props.setProperty(name, value) |
|
28045 | 322 |
} |
323 |
} |
|
28063 | 324 |
// last text line |
325 |
else if (line.endsWith("\u0002.")) { |
|
326 |
result.append(line.substring(0, len - 2)) |
|
327 |
put_result(kind, props, result.toString) |
|
328 |
result.length = 0 |
|
329 |
kind = null |
|
330 |
} |
|
331 |
// text line |
|
332 |
else { |
|
333 |
result.append(line) |
|
334 |
result.append('\n') |
|
335 |
} |
|
28045 | 336 |
} |
28063 | 337 |
//}}} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
338 |
} |
27963 | 339 |
} |
28063 | 340 |
catch { |
341 |
case e: IOException => put_result(Kind.SYSTEM, null, "Message thread: " + e.getMessage) |
|
342 |
} |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
343 |
} |
28063 | 344 |
put_result(Kind.SYSTEM, null, "Message thread terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
345 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
346 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
347 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
348 |
|
29192 | 349 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
350 |
/** main **/ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
351 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
352 |
{ |
28497
40e1cc165b05
added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm
parents:
28344
diff
changeset
|
353 |
/* isabelle version */ |
40e1cc165b05
added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm
parents:
28344
diff
changeset
|
354 |
|
40e1cc165b05
added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm
parents:
28344
diff
changeset
|
355 |
{ |
29174 | 356 |
val (msg, rc) = isabelle_system.isabelle_tool("version") |
28497
40e1cc165b05
added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm
parents:
28344
diff
changeset
|
357 |
if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg) |
40e1cc165b05
added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm
parents:
28344
diff
changeset
|
358 |
put_result(Kind.SYSTEM, null, msg) |
40e1cc165b05
added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm
parents:
28344
diff
changeset
|
359 |
} |
40e1cc165b05
added isabelle_tool version as basic integrity check of platform/distribution;
wenzelm
parents:
28344
diff
changeset
|
360 |
|
28045 | 361 |
|
29192 | 362 |
/* results */ |
363 |
||
364 |
val result_thread = new ResultThread |
|
365 |
result_thread.start |
|
366 |
||
367 |
||
368 |
/* messages */ |
|
28045 | 369 |
|
29174 | 370 |
val message_fifo = isabelle_system.mk_fifo() |
371 |
def rm_fifo() = isabelle_system.rm_fifo(message_fifo) |
|
28045 | 372 |
|
28063 | 373 |
val message_thread = new MessageThread(message_fifo) |
374 |
message_thread.start |
|
28045 | 375 |
|
376 |
||
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
377 |
/* exec process */ |
27963 | 378 |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
379 |
try { |
28501 | 380 |
val cmdline = |
29174 | 381 |
List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args |
29178 | 382 |
proc = isabelle_system.execute(true, cmdline: _*) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
383 |
} |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
384 |
catch { |
28063 | 385 |
case e: IOException => |
386 |
rm_fifo() |
|
387 |
error("Failed to execute Isabelle process: " + e.getMessage) |
|
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
388 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
389 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
390 |
|
28045 | 391 |
/* stdin/stdout */ |
392 |
||
393 |
new StdinThread(proc.getOutputStream).start |
|
394 |
new StdoutThread(proc.getInputStream).start |
|
395 |
||
396 |
||
397 |
/* exit */ |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
398 |
|
28063 | 399 |
new Thread("isabelle: exit") { |
28045 | 400 |
override def run() = { |
401 |
val rc = proc.waitFor() |
|
402 |
Thread.sleep(300) |
|
403 |
put_result(Kind.SYSTEM, null, "Exit thread terminated") |
|
404 |
put_result(Kind.EXIT, null, Integer.toString(rc)) |
|
28063 | 405 |
rm_fifo() |
28045 | 406 |
} |
28063 | 407 |
}.start |
408 |
||
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
409 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
410 |
} |