author | wenzelm |
Fri, 27 Mar 2020 12:03:20 +0100 | |
changeset 71594 | 8a298184f3f9 |
parent 69572 | 09a6a7c04b45 |
child 71597 | d025735a4090 |
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 |
|
65310 | 10 |
import java.io.{File => JFile} |
11 |
||
12 |
||
57917 | 13 |
object Isabelle_Process |
14 |
{ |
|
71594 | 15 |
def start( |
16 |
session: Session, |
|
65216 | 17 |
options: Options, |
71594 | 18 |
sessions_structure: Sessions.Structure, |
65216 | 19 |
logic: String = "", |
20 |
args: List[String] = Nil, |
|
21 |
modes: List[String] = Nil, |
|
65310 | 22 |
cwd: JFile = null, |
23 |
env: Map[String, String] = Isabelle_System.settings(), |
|
68209 | 24 |
store: Option[Sessions.Store] = None, |
65225 | 25 |
phase_changed: Session.Phase => Unit = null) |
65216 | 26 |
{ |
65225 | 27 |
if (phase_changed != null) |
28 |
session.phase_changed += Session.Consumer("Isabelle_Process")(phase_changed) |
|
29 |
||
65216 | 30 |
session.start(receiver => |
71594 | 31 |
Isabelle_Process(options, sessions_structure, logic = logic, args = args, modes = modes, |
32 |
cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache, store = store)) |
|
65216 | 33 |
} |
34 |
||
57917 | 35 |
def apply( |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
36 |
options: Options, |
71594 | 37 |
sessions_structure: Sessions.Structure, |
62634
aa3b47b32100
less physical "logic" argument, with option -l like "isabelle console" etc.;
wenzelm
parents:
62633
diff
changeset
|
38 |
logic: String = "", |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
39 |
args: List[String] = Nil, |
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
40 |
modes: List[String] = Nil, |
65310 | 41 |
cwd: JFile = null, |
42 |
env: Map[String, String] = Isabelle_System.settings(), |
|
67178 | 43 |
receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true), |
68169 | 44 |
xml_cache: XML.Cache = XML.make_cache(), |
68209 | 45 |
store: Option[Sessions.Store] = None): Prover = |
57917 | 46 |
{ |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
47 |
val channel = System_Channel() |
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
48 |
val process = |
57916 | 49 |
try { |
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
68209
diff
changeset
|
50 |
val channel_options = |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
68209
diff
changeset
|
51 |
options.string.update("system_channel_address", channel.address). |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
68209
diff
changeset
|
52 |
string.update("system_channel_password", channel.password) |
71594 | 53 |
ML_Process( |
54 |
channel_options, sessions_structure, logic = logic, args = args, modes = modes, |
|
55 |
cwd = cwd, env = env, store = store) |
|
57916 | 56 |
} |
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
68209
diff
changeset
|
57 |
catch { case exn @ ERROR(_) => channel.shutdown(); throw exn } |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
58 |
process.stdin.close |
57917 | 59 |
|
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65316
diff
changeset
|
60 |
new Prover(receiver, xml_cache, channel, process) |
57917 | 61 |
} |
57916 | 62 |
} |