src/Pure/System/isabelle_process.scala
author wenzelm
Sun May 13 16:37:36 2018 +0200 (14 months ago)
changeset 68169 395432e7516e
parent 67178 70576478bda9
child 68204 a554da2811f2
permissions -rw-r--r--
tuned signature;
wenzelm@43283
     1
/*  Title:      Pure/System/isabelle_process.scala
wenzelm@27949
     2
    Author:     Makarius
wenzelm@27949
     3
wenzelm@57916
     4
Isabelle process wrapper.
wenzelm@27949
     5
*/
wenzelm@27949
     6
wenzelm@27949
     7
package isabelle
wenzelm@27949
     8
wenzelm@55618
     9
wenzelm@65310
    10
import java.io.{File => JFile}
wenzelm@65310
    11
wenzelm@65310
    12
wenzelm@57917
    13
object Isabelle_Process
wenzelm@57917
    14
{
wenzelm@65216
    15
  def start(session: Session,
wenzelm@65216
    16
    options: Options,
wenzelm@65216
    17
    logic: String = "",
wenzelm@65216
    18
    args: List[String] = Nil,
wenzelm@65216
    19
    dirs: List[Path] = Nil,
wenzelm@65216
    20
    modes: List[String] = Nil,
wenzelm@65310
    21
    cwd: JFile = null,
wenzelm@65310
    22
    env: Map[String, String] = Isabelle_System.settings(),
wenzelm@67052
    23
    sessions: Option[Sessions.Structure] = None,
wenzelm@65225
    24
    store: Sessions.Store = Sessions.store(),
wenzelm@65225
    25
    phase_changed: Session.Phase => Unit = null)
wenzelm@65216
    26
  {
wenzelm@65225
    27
    if (phase_changed != null)
wenzelm@65225
    28
      session.phase_changed += Session.Consumer("Isabelle_Process")(phase_changed)
wenzelm@65225
    29
wenzelm@65216
    30
    session.start(receiver =>
wenzelm@65216
    31
      Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
wenzelm@65310
    32
        cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache,
wenzelm@65415
    33
        sessions = sessions, store = store))
wenzelm@65216
    34
  }
wenzelm@65216
    35
wenzelm@57917
    36
  def apply(
wenzelm@62556
    37
    options: Options,
wenzelm@62634
    38
    logic: String = "",
wenzelm@62556
    39
    args: List[String] = Nil,
wenzelm@62754
    40
    dirs: List[Path] = Nil,
wenzelm@62556
    41
    modes: List[String] = Nil,
wenzelm@65310
    42
    cwd: JFile = null,
wenzelm@65310
    43
    env: Map[String, String] = Isabelle_System.settings(),
wenzelm@67178
    44
    receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true),
wenzelm@68169
    45
    xml_cache: XML.Cache = XML.make_cache(),
wenzelm@67052
    46
    sessions: Option[Sessions.Structure] = None,
wenzelm@65345
    47
    store: Sessions.Store = Sessions.store()): Prover =
wenzelm@57917
    48
  {
wenzelm@62556
    49
    val channel = System_Channel()
wenzelm@62556
    50
    val process =
wenzelm@57916
    51
      try {
wenzelm@65310
    52
        ML_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
wenzelm@65415
    53
          cwd = cwd, env = env, sessions = sessions, store = store, channel = Some(channel))
wenzelm@57916
    54
      }
wenzelm@62556
    55
      catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
wenzelm@62556
    56
    process.stdin.close
wenzelm@57917
    57
wenzelm@65345
    58
    new Prover(receiver, xml_cache, channel, process)
wenzelm@57917
    59
  }
wenzelm@57916
    60
}