author | wenzelm |
Thu, 27 May 2010 12:35:40 +0200 | |
changeset 37132 | 10ef4da1c314 |
parent 37121 | 8e51fc35d59f |
child 37689 | 628eabe2213a |
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 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
22 |
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
|
23 |
//{{{ 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
|
24 |
// 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
|
25 |
val SYSTEM = Value("SYSTEM") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
26 |
// Posix channels/events |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
27 |
val STDIN = Value("STDIN") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
28 |
val STDOUT = Value("STDOUT") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
29 |
val SIGNAL = Value("SIGNAL") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
30 |
val EXIT = Value("EXIT") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
31 |
// 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
|
32 |
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
|
33 |
val STATUS = Value("STATUS") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
34 |
val WRITELN = Value("WRITELN") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
35 |
val TRACING = Value("TRACING") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
36 |
val WARNING = Value("WARNING") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
37 |
val ERROR = Value("ERROR") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
38 |
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
|
39 |
// 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
|
40 |
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
|
41 |
('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
|
42 |
('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
|
43 |
('C' : Int) -> Kind.WRITELN, |
37121
8e51fc35d59f
eliminated obsolete priority message from Isabelle_Process protocol;
wenzelm
parents:
37044
diff
changeset
|
44 |
('D' : Int) -> Kind.TRACING, |
8e51fc35d59f
eliminated obsolete priority message from Isabelle_Process protocol;
wenzelm
parents:
37044
diff
changeset
|
45 |
('E' : Int) -> Kind.WARNING, |
8e51fc35d59f
eliminated obsolete priority message from Isabelle_Process protocol;
wenzelm
parents:
37044
diff
changeset
|
46 |
('F' : Int) -> Kind.ERROR, |
8e51fc35d59f
eliminated obsolete priority message from Isabelle_Process protocol;
wenzelm
parents:
37044
diff
changeset
|
47 |
('G' : Int) -> Kind.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
|
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) |
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
53 |
// message markup |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
54 |
val markup = Map( |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
55 |
Kind.INIT -> Markup.INIT, |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
56 |
Kind.STATUS -> Markup.STATUS, |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
57 |
Kind.WRITELN -> Markup.WRITELN, |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
58 |
Kind.TRACING -> Markup.TRACING, |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
59 |
Kind.WARNING -> Markup.WARNING, |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
60 |
Kind.ERROR -> Markup.ERROR, |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
61 |
Kind.DEBUG -> Markup.DEBUG, |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
62 |
Kind.SYSTEM -> Markup.SYSTEM, |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
63 |
Kind.STDIN -> Markup.STDIN, |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
64 |
Kind.STDOUT -> Markup.STDOUT, |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
65 |
Kind.SIGNAL -> Markup.SIGNAL, |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
66 |
Kind.EXIT -> Markup.EXIT) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
67 |
//}}} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
68 |
def is_raw(kind: Value) = |
28045 | 69 |
kind == STDOUT |
27990 | 70 |
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
|
71 |
kind == SYSTEM || |
27990 | 72 |
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
|
73 |
kind == EXIT |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
74 |
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
|
75 |
kind == SYSTEM || |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
76 |
kind == STDIN || |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
77 |
kind == SIGNAL || |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
78 |
kind == EXIT || |
28498 | 79 |
kind == STATUS |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
80 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
81 |
|
34100 | 82 |
class Result(val kind: Kind.Value, val props: List[(String, String)], val body: List[XML.Tree]) |
83 |
{ |
|
37044
d93b849cbecd
simplified message markup, using plain XML.Elem directly;
wenzelm
parents:
37038
diff
changeset
|
84 |
def message = XML.Elem(Kind.markup(kind), props, body) |
34100 | 85 |
|
86 |
override def toString: String = |
|
87 |
{ |
|
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29506
diff
changeset
|
88 |
val res = |
34100 | 89 |
if (kind == Kind.STATUS) body.map(_.toString).mkString |
36735
42b7f881f5fc
output symbolic pretty printing markup and format in the front end;
wenzelm
parents:
34215
diff
changeset
|
90 |
else Pretty.string_of(body) |
29572
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
91 |
if (props.isEmpty) |
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
92 |
kind.toString + " [[" + res + "]]" |
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
93 |
else |
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
94 |
kind.toString + " " + |
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
95 |
(for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]" |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
96 |
} |
29192 | 97 |
def is_raw = Kind.is_raw(kind) |
98 |
def is_control = Kind.is_control(kind) |
|
99 |
def is_system = Kind.is_system(kind) |
|
34109 | 100 |
|
34215 | 101 |
def is_ready = kind == Kind.STATUS && body == List(XML.Elem(Markup.READY, Nil, Nil)) |
102 |
||
34117 | 103 |
def cache(c: XML.Cache): Result = |
104 |
new Result(kind, c.cache_props(props), c.cache_trees(body)) |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
105 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
106 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
107 |
|
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
108 |
|
34100 | 109 |
class Isabelle_Process(system: Isabelle_System, receiver: Actor, args: String*) |
29192 | 110 |
{ |
31797 | 111 |
import Isabelle_Process._ |
29194 | 112 |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
113 |
|
29192 | 114 |
/* demo constructor */ |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
115 |
|
29192 | 116 |
def this(args: String*) = |
32474
0818e6b1c8a6
Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents:
32448
diff
changeset
|
117 |
this(new Isabelle_System, |
34213
9e86c1ca6e51
removed obsolete version check -- sanity delegated to Isabelle_System;
wenzelm
parents:
34201
diff
changeset
|
118 |
actor { loop { react { case res => Console.println(res) } } }, args: _*) |
29174 | 119 |
|
120 |
||
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
121 |
/* process information */ |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
122 |
|
29648 | 123 |
@volatile private var proc: Process = null |
124 |
@volatile private var closing = false |
|
125 |
@volatile private var pid: String = null |
|
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 |
/* results */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
129 |
|
34100 | 130 |
private def put_result(kind: Kind.Value, props: List[(String, String)], body: List[XML.Tree]) |
29572
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
131 |
{ |
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
132 |
if (kind == Kind.INIT) { |
34214
99eefb83a35d
simplified init message -- removed redundant session property;
wenzelm
parents:
34213
diff
changeset
|
133 |
for ((Markup.PID, p) <- props) pid = p |
27963 | 134 |
} |
34100 | 135 |
receiver ! new Result(kind, props, body) |
136 |
} |
|
137 |
||
138 |
private def put_result(kind: Kind.Value, text: String) |
|
139 |
{ |
|
140 |
put_result(kind, Nil, List(XML.Text(system.symbols.decode(text)))) |
|
27992 | 141 |
} |
142 |
||
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
143 |
|
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
144 |
/* signals */ |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
145 |
|
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
146 |
def interrupt() = synchronized { |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
147 |
if (proc == null) error("Cannot interrupt Isabelle: no process") |
34100 | 148 |
if (pid == null) put_result(Kind.SYSTEM, "Cannot interrupt: unknown pid") |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
149 |
else { |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
150 |
try { |
34100 | 151 |
if (system.execute(true, "kill", "-INT", pid).waitFor == 0) |
152 |
put_result(Kind.SIGNAL, "INT") |
|
27990 | 153 |
else |
34100 | 154 |
put_result(Kind.SYSTEM, "Cannot interrupt: kill command failed") |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
155 |
} |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
156 |
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
|
157 |
} |
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 |
def kill() = synchronized { |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
161 |
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
|
162 |
else { |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
163 |
try_close() |
37132 | 164 |
Thread.sleep(500) // FIXME property!? |
34100 | 165 |
put_result(Kind.SIGNAL, "KILL") |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
166 |
proc.destroy |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
167 |
proc = null |
27990 | 168 |
pid = null |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
169 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
170 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
171 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
172 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
173 |
/* output being piped into the process */ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
174 |
|
27990 | 175 |
private val output = new LinkedBlockingQueue[String] |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
176 |
|
28045 | 177 |
private def output_raw(text: String) = synchronized { |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
178 |
if (proc == null) error("Cannot output to Isabelle: no process") |
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
179 |
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
|
180 |
output.put(text) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
181 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
182 |
|
28303 | 183 |
def output_sync(text: String) = |
28045 | 184 |
output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
185 |
|
27963 | 186 |
|
187 |
def command(text: String) = |
|
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
188 |
output_sync("Isabelle.command " + Isabelle_Syntax.encode_string(text)) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
189 |
|
29572
e3a99d957392
replaced java.util.Properties by plain association list;
wenzelm
parents:
29522
diff
changeset
|
190 |
def command(props: List[(String, String)], text: String) = |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
191 |
output_sync("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " + |
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
192 |
Isabelle_Syntax.encode_string(text)) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
193 |
|
27963 | 194 |
def ML(text: String) = |
32448
a89f876731c5
moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
wenzelm
parents:
31797
diff
changeset
|
195 |
output_sync("ML_val " + Isabelle_Syntax.encode_string(text)) |
27949
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 |
def close() = synchronized { // FIXME watchdog/timeout |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
198 |
output_raw("\u0000") |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
199 |
closing = true |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
200 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
201 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
202 |
def try_close() = synchronized { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
203 |
if (proc != null && !closing) { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
204 |
try { close() } |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
205 |
catch { case _: RuntimeException => } |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
206 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
207 |
} |
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 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
210 |
/* stdin */ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
211 |
|
34213
9e86c1ca6e51
removed obsolete version check -- sanity delegated to Isabelle_System;
wenzelm
parents:
34201
diff
changeset
|
212 |
private class Stdin_Thread(out_stream: OutputStream) extends Thread("isabelle: stdin") { |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
213 |
override def run() = { |
34201
c95dcd12f48a
separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
34117
diff
changeset
|
214 |
val writer = new BufferedWriter(new OutputStreamWriter(out_stream, Standard_System.charset)) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
215 |
var finished = false |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
216 |
while (!finished) { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
217 |
try { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
218 |
//{{{ |
27955
4c32c5e75eca
use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
wenzelm
parents:
27949
diff
changeset
|
219 |
val s = output.take |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
220 |
if (s == "\u0000") { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
221 |
writer.close |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
222 |
finished = true |
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 |
else { |
34100 | 225 |
put_result(Kind.STDIN, s) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
226 |
writer.write(s) |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
227 |
writer.flush |
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 |
//}}} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
230 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
231 |
catch { |
34100 | 232 |
case e: IOException => put_result(Kind.SYSTEM, "Stdin thread: " + e.getMessage) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
233 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
234 |
} |
34100 | 235 |
put_result(Kind.SYSTEM, "Stdin thread terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
236 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
237 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
238 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
239 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
240 |
/* stdout */ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
241 |
|
34213
9e86c1ca6e51
removed obsolete version check -- sanity delegated to Isabelle_System;
wenzelm
parents:
34201
diff
changeset
|
242 |
private class Stdout_Thread(in_stream: InputStream) extends Thread("isabelle: stdout") { |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
243 |
override def run() = { |
34201
c95dcd12f48a
separate Standard_System (Cygwin/Posix compatibility) vs. Isabelle_System (settings environment etc.);
wenzelm
parents:
34117
diff
changeset
|
244 |
val reader = new BufferedReader(new InputStreamReader(in_stream, Standard_System.charset)) |
28045 | 245 |
var result = new StringBuilder(100) |
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 |
var finished = false |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
248 |
while (!finished) { |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
249 |
try { |
28045 | 250 |
//{{{ |
251 |
var c = -1 |
|
252 |
var done = false |
|
253 |
while (!done && (result.length == 0 || reader.ready)) { |
|
254 |
c = reader.read |
|
255 |
if (c >= 0) result.append(c.asInstanceOf[Char]) |
|
256 |
else done = true |
|
257 |
} |
|
258 |
if (result.length > 0) { |
|
34100 | 259 |
put_result(Kind.STDOUT, result.toString) |
28045 | 260 |
result.length = 0 |
27949
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 |
else { |
28045 | 263 |
reader.close |
264 |
finished = true |
|
265 |
try_close() |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
266 |
} |
28045 | 267 |
//}}} |
27963 | 268 |
} |
269 |
catch { |
|
34100 | 270 |
case e: IOException => put_result(Kind.SYSTEM, "Stdout thread: " + e.getMessage) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
271 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
272 |
} |
34100 | 273 |
put_result(Kind.SYSTEM, "Stdout thread terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
274 |
} |
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 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
277 |
|
28045 | 278 |
/* messages */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
279 |
|
34213
9e86c1ca6e51
removed obsolete version check -- sanity delegated to Isabelle_System;
wenzelm
parents:
34201
diff
changeset
|
280 |
private class Message_Thread(fifo: String) extends Thread("isabelle: messages") |
34100 | 281 |
{ |
282 |
private class Protocol_Error(msg: String) extends Exception(msg) |
|
283 |
override def run() |
|
284 |
{ |
|
285 |
val stream = system.fifo_stream(fifo) |
|
286 |
val default_buffer = new Array[Byte](65536) |
|
287 |
var c = -1 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
288 |
|
34100 | 289 |
def read_chunk(): List[XML.Tree] = |
290 |
{ |
|
291 |
//{{{ |
|
292 |
// chunk size |
|
293 |
var n = 0 |
|
294 |
c = stream.read |
|
295 |
while (48 <= c && c <= 57) { |
|
296 |
n = 10 * n + (c - 48) |
|
297 |
c = stream.read |
|
298 |
} |
|
299 |
if (c != 10) throw new Protocol_Error("bad message chunk header") |
|
300 |
||
301 |
// chunk content |
|
302 |
val buf = |
|
303 |
if (n <= default_buffer.size) default_buffer |
|
304 |
else new Array[Byte](n) |
|
305 |
||
306 |
var i = 0 |
|
307 |
var m = 0 |
|
308 |
do { |
|
309 |
m = stream.read(buf, i, n - i) |
|
310 |
i += m |
|
311 |
} while (m > 0 && n > i) |
|
312 |
||
313 |
if (i != n) throw new Protocol_Error("bad message chunk content") |
|
314 |
||
315 |
YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n)) |
|
316 |
//}}} |
|
317 |
} |
|
318 |
||
319 |
do { |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
320 |
try { |
34100 | 321 |
//{{{ |
322 |
c = stream.read |
|
323 |
var non_sync = 0 |
|
324 |
while (c >= 0 && c != 2) { |
|
325 |
non_sync += 1 |
|
326 |
c = stream.read |
|
28063 | 327 |
} |
34100 | 328 |
if (non_sync > 0) |
329 |
throw new Protocol_Error("lost synchronization -- skipping " + non_sync + " bytes") |
|
330 |
if (c == 2) { |
|
331 |
val header = read_chunk() |
|
332 |
val body = read_chunk() |
|
333 |
header match { |
|
334 |
case List(XML.Elem(name, props, Nil)) |
|
335 |
if name.size == 1 && Kind.code.isDefinedAt(name(0)) => |
|
336 |
put_result(Kind.code(name(0)), props, body) |
|
337 |
case _ => throw new Protocol_Error("bad header: " + header.toString) |
|
28063 | 338 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
339 |
} |
34100 | 340 |
//}}} |
27963 | 341 |
} |
28063 | 342 |
catch { |
34100 | 343 |
case e: IOException => |
344 |
put_result(Kind.SYSTEM, "Cannot read message:\n" + e.getMessage) |
|
345 |
case e: Protocol_Error => |
|
346 |
put_result(Kind.SYSTEM, "Malformed message:\n" + e.getMessage) |
|
28063 | 347 |
} |
34100 | 348 |
} while (c != -1) |
349 |
stream.close |
|
350 |
try_close() |
|
351 |
||
352 |
put_result(Kind.SYSTEM, "Message thread terminated") |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
353 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
354 |
} |
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 |
|
29192 | 357 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
358 |
/** main **/ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
359 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
360 |
{ |
29192 | 361 |
/* messages */ |
28045 | 362 |
|
34100 | 363 |
val message_fifo = system.mk_fifo() |
364 |
def rm_fifo() = system.rm_fifo(message_fifo) |
|
28045 | 365 |
|
34213
9e86c1ca6e51
removed obsolete version check -- sanity delegated to Isabelle_System;
wenzelm
parents:
34201
diff
changeset
|
366 |
val message_thread = new Message_Thread(message_fifo) |
28063 | 367 |
message_thread.start |
28045 | 368 |
|
369 |
||
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
370 |
/* exec process */ |
27963 | 371 |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
372 |
try { |
34100 | 373 |
val cmdline = List(system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args |
374 |
proc = system.execute(true, cmdline: _*) |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
375 |
} |
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
376 |
catch { |
28063 | 377 |
case e: IOException => |
378 |
rm_fifo() |
|
379 |
error("Failed to execute Isabelle process: " + e.getMessage) |
|
27993
6dd90ef9f927
simplified exceptions: use plain error function / RuntimeException;
wenzelm
parents:
27992
diff
changeset
|
380 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
381 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
382 |
|
28045 | 383 |
/* stdin/stdout */ |
384 |
||
34213
9e86c1ca6e51
removed obsolete version check -- sanity delegated to Isabelle_System;
wenzelm
parents:
34201
diff
changeset
|
385 |
new Stdin_Thread(proc.getOutputStream).start |
9e86c1ca6e51
removed obsolete version check -- sanity delegated to Isabelle_System;
wenzelm
parents:
34201
diff
changeset
|
386 |
new Stdout_Thread(proc.getInputStream).start |
28045 | 387 |
|
388 |
||
389 |
/* exit */ |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
390 |
|
28063 | 391 |
new Thread("isabelle: exit") { |
28045 | 392 |
override def run() = { |
393 |
val rc = proc.waitFor() |
|
37132 | 394 |
Thread.sleep(300) // FIXME property!? |
34100 | 395 |
put_result(Kind.SYSTEM, "Exit thread terminated") |
396 |
put_result(Kind.EXIT, rc.toString) |
|
28063 | 397 |
rm_fifo() |
28045 | 398 |
} |
28063 | 399 |
}.start |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
400 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
401 |
} |