1/*  Title:      Pure/System/isabelle_process.scala
2    Author:     Makarius
3
4Isabelle process wrapper.
5*/
6
7package isabelle
8
9
10import java.io.{File => JFile}
11
12
13object Isabelle_Process
14{
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,
21    cwd: JFile = null,
22    env: Map[String, String] = Isabelle_System.settings(),
23    sessions_structure: Option[Sessions.Structure] = None,
24    store: Option[Sessions.Store] = None,
25    phase_changed: Session.Phase => Unit = null)
26  {
27    if (phase_changed != null)
28      session.phase_changed += Session.Consumer("Isabelle_Process")(phase_changed)
29
30    session.start(receiver =>
31      Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
32        cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache,
33        sessions_structure = sessions_structure, store = store))
34  }
35
36  def apply(
37    options: Options,
38    logic: String = "",
39    args: List[String] = Nil,
40    dirs: List[Path] = Nil,
41    modes: List[String] = Nil,
42    cwd: JFile = null,
43    env: Map[String, String] = Isabelle_System.settings(),
44    receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true),
45    xml_cache: XML.Cache = XML.make_cache(),
46    sessions_structure: Option[Sessions.Structure] = None,
47    store: Option[Sessions.Store] = None): Prover =
48  {
49    val channel = System_Channel()
50    val process =
51      try {
52        val channel_options =
53          options.string.update("system_channel_address", channel.address).
54            string.update("system_channel_password", channel.password)
55        ML_Process(channel_options, logic = logic, args = args, dirs = dirs, modes = modes,
56            cwd = cwd, env = env, sessions_structure = sessions_structure, store = store)
57      }
58      catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
59    process.stdin.close
60
61    new Prover(receiver, xml_cache, channel, process)
62  }
63}
64