author | wenzelm |
Sun, 14 Feb 2016 13:38:31 +0100 | |
changeset 62309 | 96c9a259d275 |
parent 62308 | 9b9547c9a6ed |
child 62545 | 8ebffdaf2ce2 |
permissions | -rw-r--r-- |
43283 | 1 |
/* Title: Pure/System/isabelle_process.scala |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
3 |
|
57916 | 4 |
Isabelle process wrapper. |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
5 |
*/ |
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 |
package isabelle |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
8 |
|
55618 | 9 |
|
57917 | 10 |
object Isabelle_Process |
11 |
{ |
|
12 |
def apply( |
|
13 |
receiver: Prover.Message => Unit = Console.println(_), |
|
62296 | 14 |
prover_args: String = ""): Isabelle_Process = |
57917 | 15 |
{ |
16 |
val system_channel = System_Channel() |
|
17 |
val system_process = |
|
57916 | 18 |
try { |
62296 | 19 |
val script = |
62308 | 20 |
File.shell_quote(Isabelle_System.getenv_strict("ISABELLE_PROCESS")) + |
21 |
" -P " + system_channel.server_name + |
|
62296 | 22 |
(if (prover_args == "") "" else " " + prover_args) |
23 |
val process = Bash.process(null, null, false, "-c", script) |
|
57916 | 24 |
process.stdin.close |
25 |
process |
|
26 |
} |
|
60215 | 27 |
catch { case exn @ ERROR(_) => system_channel.accepted(); throw exn } |
57917 | 28 |
|
29 |
new Isabelle_Process(receiver, system_channel, system_process) |
|
30 |
} |
|
57916 | 31 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
32 |
|
57917 | 33 |
class Isabelle_Process private( |
34 |
receiver: Prover.Message => Unit, |
|
35 |
system_channel: System_Channel, |
|
36 |
system_process: Prover.System_Process) |
|
37 |
extends Prover(receiver, system_channel, system_process) |
|
62309 | 38 |
{ |
39 |
def encode(s: String): String = Symbol.encode(s) |
|
40 |
def decode(s: String): String = Symbol.decode(s) |
|
41 |
} |