| author | wenzelm |
| Mon, 13 Oct 2014 22:43:29 +0200 | |
| changeset 58668 | 1891f17c6124 |
| parent 57917 | 8ce97e5d545f |
| child 60215 | 5fb4990dfc73 |
| 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(_), |
|
14 |
prover_args: List[String] = Nil): Isabelle_Process = |
|
15 |
{
|
|
16 |
val system_channel = System_Channel() |
|
17 |
val system_process = |
|
| 57916 | 18 |
try {
|
19 |
val cmdline = |
|
20 |
Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
|
|
21 |
(system_channel.prover_args ::: prover_args) |
|
22 |
val process = |
|
23 |
new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with |
|
| 57917 | 24 |
Prover.System_Process |
| 57916 | 25 |
process.stdin.close |
26 |
process |
|
27 |
} |
|
28 |
catch { case exn @ ERROR(_) => system_channel.accepted(); throw(exn) }
|
|
| 57917 | 29 |
|
30 |
new Isabelle_Process(receiver, system_channel, system_process) |
|
31 |
} |
|
| 57916 | 32 |
} |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
33 |
|
| 57917 | 34 |
class Isabelle_Process private( |
35 |
receiver: Prover.Message => Unit, |
|
36 |
system_channel: System_Channel, |
|
37 |
system_process: Prover.System_Process) |
|
38 |
extends Prover(receiver, system_channel, system_process) |
|
39 |
{
|
|
40 |
def encode(s: String): String = Symbol.encode(s) |
|
41 |
def decode(s: String): String = Symbol.decode(s) |
|
42 |
} |
|
43 |