src/Pure/System/isabelle_process.scala
author wenzelm
Thu May 17 15:38:36 2018 +0200 (11 months ago)
changeset 68204 a554da2811f2
parent 68169 395432e7516e
child 68209 aeffd8f1f079
permissions -rw-r--r--
clarified signature;
     1 /*  Title:      Pure/System/isabelle_process.scala
     2     Author:     Makarius
     3 
     4 Isabelle process wrapper.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.io.{File => JFile}
    11 
    12 
    13 object 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: Sessions.Store = Sessions.store(),
    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: Sessions.Store = Sessions.store()): Prover =
    48   {
    49     val channel = System_Channel()
    50     val process =
    51       try {
    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))
    54       }
    55       catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
    56     process.stdin.close
    57 
    58     new Prover(receiver, xml_cache, channel, process)
    59   }
    60 }