| author | wenzelm | 
| Wed, 17 Jun 2015 22:30:22 +0200 | |
| changeset 60511 | 5e67a223a141 | 
| parent 60215 | 5fb4990dfc73 | 
| child 60991 | 2fc5a44346b5 | 
| 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 | } | |
| 60215 | 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 |