5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 class Isabelle_Process( |
10 object Isabelle_Process |
11 receiver: Prover.Message => Unit = Console.println(_), |
11 { |
12 prover_args: List[String] = Nil) extends Prover(receiver, |
12 def apply( |
13 { |
13 receiver: Prover.Message => Unit = Console.println(_), |
14 val system_channel = System_Channel() |
14 prover_args: List[String] = Nil): Isabelle_Process = |
|
15 { |
|
16 val system_channel = System_Channel() |
|
17 val system_process = |
15 try { |
18 try { |
16 val cmdline = |
19 val cmdline = |
17 Isabelle_System.getenv_strict("ISABELLE_PROCESS") :: |
20 Isabelle_System.getenv_strict("ISABELLE_PROCESS") :: |
18 (system_channel.prover_args ::: prover_args) |
21 (system_channel.prover_args ::: prover_args) |
19 val process = |
22 val process = |
20 new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with |
23 new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with |
21 Prover.System_Process { def channel = system_channel } |
24 Prover.System_Process |
22 process.stdin.close |
25 process.stdin.close |
23 process |
26 process |
24 } |
27 } |
25 catch { case exn @ ERROR(_) => system_channel.accepted(); throw(exn) } |
28 catch { case exn @ ERROR(_) => system_channel.accepted(); throw(exn) } |
26 }) |
29 |
27 { |
30 new Isabelle_Process(receiver, system_channel, system_process) |
28 def encode(s: String): String = Symbol.encode(s) |
31 } |
29 def decode(s: String): String = Symbol.decode(s) |
|
30 } |
32 } |
31 |
33 |
|
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 |