| author | nipkow | 
| Mon, 17 Oct 2016 17:33:07 +0200 | |
| changeset 64272 | f76b6dda2e56 | 
| parent 62754 | c35012b86e6f | 
| child 65216 | 060a8a1f2dec | 
| 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( | |
| 62556 
c115e69f457f
more abstract Session.start, without prover command-line;
 wenzelm parents: 
62555diff
changeset | 13 | options: Options, | 
| 62634 
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
 wenzelm parents: 
62633diff
changeset | 14 | logic: String = "", | 
| 62556 
c115e69f457f
more abstract Session.start, without prover command-line;
 wenzelm parents: 
62555diff
changeset | 15 | args: List[String] = Nil, | 
| 62754 
c35012b86e6f
proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
 wenzelm parents: 
62668diff
changeset | 16 | dirs: List[Path] = Nil, | 
| 62556 
c115e69f457f
more abstract Session.start, without prover command-line;
 wenzelm parents: 
62555diff
changeset | 17 | modes: List[String] = Nil, | 
| 62633 | 18 | receiver: Prover.Receiver = Console.println(_), | 
| 19 | store: Sessions.Store = Sessions.store()): Isabelle_Process = | |
| 57917 | 20 |   {
 | 
| 62556 
c115e69f457f
more abstract Session.start, without prover command-line;
 wenzelm parents: 
62555diff
changeset | 21 | val channel = System_Channel() | 
| 
c115e69f457f
more abstract Session.start, without prover command-line;
 wenzelm parents: 
62555diff
changeset | 22 | val process = | 
| 57916 | 23 |       try {
 | 
| 62754 
c35012b86e6f
proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
 wenzelm parents: 
62668diff
changeset | 24 | ML_Process(options, logic = logic, args = args, dirs = dirs, | 
| 
c35012b86e6f
proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
 wenzelm parents: 
62668diff
changeset | 25 | modes = modes, store = store, channel = Some(channel)) | 
| 57916 | 26 | } | 
| 62556 
c115e69f457f
more abstract Session.start, without prover command-line;
 wenzelm parents: 
62555diff
changeset | 27 |       catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
 | 
| 
c115e69f457f
more abstract Session.start, without prover command-line;
 wenzelm parents: 
62555diff
changeset | 28 | process.stdin.close | 
| 57917 | 29 | |
| 62556 
c115e69f457f
more abstract Session.start, without prover command-line;
 wenzelm parents: 
62555diff
changeset | 30 | new Isabelle_Process(receiver, channel, process) | 
| 57917 | 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( | 
| 62556 
c115e69f457f
more abstract Session.start, without prover command-line;
 wenzelm parents: 
62555diff
changeset | 35 | receiver: Prover.Receiver, channel: System_Channel, process: Prover.System_Process) | 
| 
c115e69f457f
more abstract Session.start, without prover command-line;
 wenzelm parents: 
62555diff
changeset | 36 | extends Prover(receiver, channel, process) | 
| 62309 | 37 | {
 | 
| 38 | def encode(s: String): String = Symbol.encode(s) | |
| 39 | def decode(s: String): String = Symbol.decode(s) | |
| 40 | } |