author | wenzelm |
Fri, 18 May 2018 17:09:55 +0200 | |
changeset 68209 | aeffd8f1f079 |
parent 68204 | a554da2811f2 |
child 69572 | 09a6a7c04b45 |
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 |
{ |
|
65216 | 15 |
def start(session: Session, |
16 |
options: Options, |
|
17 |
logic: String = "", |
|
18 |
args: List[String] = Nil, |
|
19 |
dirs: List[Path] = Nil, |
|
20 |
modes: List[String] = Nil, |
|
65310 | 21 |
cwd: JFile = null, |
22 |
env: Map[String, String] = Isabelle_System.settings(), |
|
68204 | 23 |
sessions_structure: Option[Sessions.Structure] = None, |
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 => |
31 |
Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes, |
|
65310 | 32 |
cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache, |
68204 | 33 |
sessions_structure = sessions_structure, store = store)) |
65216 | 34 |
} |
35 |
||
57917 | 36 |
def apply( |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
37 |
options: Options, |
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, |
62754
c35012b86e6f
proper session dirs for "isabelle jedit" and "isabelle console" with options -d and -l;
wenzelm
parents:
62668
diff
changeset
|
40 |
dirs: List[Path] = Nil, |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
41 |
modes: List[String] = Nil, |
65310 | 42 |
cwd: JFile = null, |
43 |
env: Map[String, String] = Isabelle_System.settings(), |
|
67178 | 44 |
receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true), |
68169 | 45 |
xml_cache: XML.Cache = XML.make_cache(), |
68204 | 46 |
sessions_structure: Option[Sessions.Structure] = None, |
68209 | 47 |
store: Option[Sessions.Store] = None): Prover = |
57917 | 48 |
{ |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
49 |
val channel = System_Channel() |
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
50 |
val process = |
57916 | 51 |
try { |
68204 | 52 |
ML_Process(options, logic = logic, args = args, dirs = dirs, modes = modes, cwd = cwd, |
53 |
env = env, sessions_structure = sessions_structure, store = store, channel = Some(channel)) |
|
57916 | 54 |
} |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
55 |
catch { case exn @ ERROR(_) => channel.accepted(); throw exn } |
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62555
diff
changeset
|
56 |
process.stdin.close |
57917 | 57 |
|
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65316
diff
changeset
|
58 |
new Prover(receiver, xml_cache, channel, process) |
57917 | 59 |
} |
57916 | 60 |
} |