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