| author | wenzelm |
| Fri, 27 Mar 2020 22:01:27 +0100 | |
| changeset 71601 | 97ccf48c2f0c |
| parent 71598 | 269dc4bf1f40 |
| child 71604 | c6fa217c9d5e |
| 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 |
{
|
|
| 71597 | 15 |
def apply( |
| 71594 | 16 |
session: Session, |
| 65216 | 17 |
options: Options, |
| 71594 | 18 |
sessions_structure: Sessions.Structure, |
| 71598 | 19 |
store: Sessions.Store, |
| 65216 | 20 |
logic: String = "", |
21 |
args: List[String] = Nil, |
|
22 |
modes: List[String] = Nil, |
|
| 65310 | 23 |
cwd: JFile = null, |
24 |
env: Map[String, String] = Isabelle_System.settings(), |
|
| 65225 | 25 |
phase_changed: Session.Phase => Unit = null) |
| 65216 | 26 |
{
|
|
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
27 |
val channel = System_Channel() |
|
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
28 |
val process = |
| 57916 | 29 |
try {
|
|
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
68209
diff
changeset
|
30 |
val channel_options = |
|
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
68209
diff
changeset
|
31 |
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
|
32 |
string.update("system_channel_password", channel.password)
|
| 71598 | 33 |
ML_Process(channel_options, sessions_structure, store, |
34 |
logic = logic, args = args, modes = modes, cwd = cwd, env = env) |
|
| 57916 | 35 |
} |
|
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
68209
diff
changeset
|
36 |
catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
|
|
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
37 |
process.stdin.close |
| 57917 | 38 |
|
| 71597 | 39 |
if (phase_changed != null) |
40 |
session.phase_changed += Session.Consumer("Isabelle_Process")(phase_changed)
|
|
41 |
||
42 |
session.start(receiver => new Prover(receiver, session.xml_cache, channel, process)) |
|
| 57917 | 43 |
} |
| 57916 | 44 |
} |