11 { |
11 { |
12 def apply( |
12 def apply( |
13 options: Options, |
13 options: Options, |
14 logic: String = "", |
14 logic: String = "", |
15 args: List[String] = Nil, |
15 args: List[String] = Nil, |
|
16 dirs: List[Path] = Nil, |
16 modes: List[String] = Nil, |
17 modes: List[String] = Nil, |
17 receiver: Prover.Receiver = Console.println(_), |
18 receiver: Prover.Receiver = Console.println(_), |
18 store: Sessions.Store = Sessions.store()): Isabelle_Process = |
19 store: Sessions.Store = Sessions.store()): Isabelle_Process = |
19 { |
20 { |
20 val channel = System_Channel() |
21 val channel = System_Channel() |
21 val process = |
22 val process = |
22 try { |
23 try { |
23 ML_Process(options, logic = logic, args = args, modes = modes, store = store, |
24 ML_Process(options, logic = logic, args = args, dirs = dirs, |
24 channel = Some(channel)) |
25 modes = modes, store = store, channel = Some(channel)) |
25 } |
26 } |
26 catch { case exn @ ERROR(_) => channel.accepted(); throw exn } |
27 catch { case exn @ ERROR(_) => channel.accepted(); throw exn } |
27 process.stdin.close |
28 process.stdin.close |
28 |
29 |
29 new Isabelle_Process(receiver, channel, process) |
30 new Isabelle_Process(receiver, channel, process) |