author | wenzelm |
Tue, 12 Aug 2014 18:36:43 +0200 | |
changeset 57916 | 2c2c24dbf0a4 |
parent 57915 | 448325de6e4f |
child 57917 | 8ce97e5d545f |
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 |
|
45055
55274f7e306b
explicit option for socket vs. fifo communication;
wenzelm
parents:
45027
diff
changeset
|
10 |
class Isabelle_Process( |
56831
e3ccf0809d51
prefer scala.Console with its support for thread-local redirection;
wenzelm
parents:
56794
diff
changeset
|
11 |
receiver: Prover.Message => Unit = Console.println(_), |
57916 | 12 |
prover_args: List[String] = Nil) extends Prover(receiver, |
13 |
{ |
|
14 |
val system_channel = System_Channel() |
|
15 |
try { |
|
16 |
val cmdline = |
|
17 |
Isabelle_System.getenv_strict("ISABELLE_PROCESS") :: |
|
18 |
(system_channel.prover_args ::: prover_args) |
|
19 |
val process = |
|
20 |
new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with |
|
21 |
Prover.System_Process { def channel = system_channel } |
|
22 |
process.stdin.close |
|
23 |
process |
|
24 |
} |
|
25 |
catch { case exn @ ERROR(_) => system_channel.accepted(); throw(exn) } |
|
26 |
}) |
|
29192 | 27 |
{ |
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
28 |
def encode(s: String): String = Symbol.encode(s) |
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
29 |
def decode(s: String): String = Symbol.decode(s) |
57916 | 30 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
31 |