author | wenzelm |
Tue, 14 Mar 2017 11:48:15 +0100 | |
changeset 65225 | ec9ec04546fc |
parent 65218 | 102b8e092860 |
child 65310 | da9f1ef8ef7c |
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 |
{ |
|
65216 | 12 |
def start(session: Session, |
13 |
options: Options, |
|
14 |
logic: String = "", |
|
15 |
args: List[String] = Nil, |
|
16 |
dirs: List[Path] = Nil, |
|
17 |
modes: List[String] = Nil, |
|
65225 | 18 |
store: Sessions.Store = Sessions.store(), |
19 |
phase_changed: Session.Phase => Unit = null) |
|
65216 | 20 |
{ |
65225 | 21 |
if (phase_changed != null) |
22 |
session.phase_changed += Session.Consumer("Isabelle_Process")(phase_changed) |
|
23 |
||
65216 | 24 |
session.start(receiver => |
25 |
Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes, |
|
65218 | 26 |
receiver = receiver, xml_cache = session.xml_cache, store = store)) |
65216 | 27 |
} |
28 |
||
57917 | 29 |
def apply( |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
30 |
options: Options, |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
31 |
logic: String = "", |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
32 |
args: List[String] = Nil, |
62754
c35012b86e6f
proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
wenzelm
parents:
62668
diff
changeset
|
33 |
dirs: List[Path] = Nil, |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
34 |
modes: List[String] = Nil, |
62633 | 35 |
receiver: Prover.Receiver = Console.println(_), |
65218 | 36 |
xml_cache: XML.Cache = new XML.Cache(), |
62633 | 37 |
store: Sessions.Store = Sessions.store()): Isabelle_Process = |
57917 | 38 |
{ |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
39 |
val channel = System_Channel() |
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
40 |
val process = |
57916 | 41 |
try { |
62754
c35012b86e6f
proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
wenzelm
parents:
62668
diff
changeset
|
42 |
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:
62668
diff
changeset
|
43 |
modes = modes, store = store, channel = Some(channel)) |
57916 | 44 |
} |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
45 |
catch { case exn @ ERROR(_) => channel.accepted(); throw exn } |
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
46 |
process.stdin.close |
57917 | 47 |
|
65218 | 48 |
new Isabelle_Process(receiver, xml_cache, channel, process) |
57917 | 49 |
} |
57916 | 50 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
51 |
|
57917 | 52 |
class Isabelle_Process private( |
65218 | 53 |
receiver: Prover.Receiver, |
54 |
xml_cache: XML.Cache, |
|
55 |
channel: System_Channel, |
|
56 |
process: Prover.System_Process) |
|
57 |
extends Prover(receiver, xml_cache, channel, process) |
|
62309 | 58 |
{ |
59 |
def encode(s: String): String = Symbol.encode(s) |
|
60 |
def decode(s: String): String = Symbol.decode(s) |
|
61 |
} |