1.1 --- a/src/Pure/System/isabelle_process.scala	Tue Aug 12 16:20:09 2014 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Aug 12 17:28:07 2014 +0200
     1.3 @@ -15,12 +15,31 @@
     1.4    receiver: Prover.Message => Unit = Console.println(_),
     1.5    prover_args: List[String] = Nil)
     1.6  {
     1.7 +  /* system process -- default implementation */
     1.8 +
     1.9 +  protected val system_process: Prover.System_Process =
    1.10 +  {
    1.11 +    val system_channel = System_Channel()
    1.12 +    try {
    1.13 +      val cmdline =
    1.14 +        Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
    1.15 +          (system_channel.prover_args ::: prover_args)
    1.16 +      val process =
    1.17 +        new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with
    1.18 +          Prover.System_Process { def channel = system_channel }
    1.19 +      process.stdin.close
    1.20 +      process
    1.21 +    }
    1.22 +    catch { case exn @ ERROR(_) => system_channel.accepted(); throw(exn) }
    1.23 +  }
    1.24 +
    1.25 +
    1.26    /* text and tree data */
    1.27  
    1.28    def encode(s: String): String = Symbol.encode(s)
    1.29    def decode(s: String): String = Symbol.decode(s)
    1.30  
    1.31 -  val xml_cache = new XML.Cache()
    1.32 +  val xml_cache: XML.Cache = new XML.Cache()
    1.33  
    1.34  
    1.35    /* output */
    1.36 @@ -37,7 +56,7 @@
    1.37  
    1.38    private def output(kind: String, props: Properties.T, body: XML.Body)
    1.39    {
    1.40 -    if (kind == Markup.INIT) system_channel.accepted()
    1.41 +    if (kind == Markup.INIT) system_process.channel.accepted()
    1.42  
    1.43      val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body))
    1.44      val reports = Protocol.message_reports(props, body)
    1.45 @@ -53,25 +72,15 @@
    1.46  
    1.47    /** process manager **/
    1.48  
    1.49 -  def command_line(channel: System_Channel, args: List[String]): List[String] =
    1.50 -    Isabelle_System.getenv_strict("ISABELLE_PROCESS") :: (channel.isabelle_args ::: args)
    1.51 -
    1.52 -  private val system_channel = System_Channel()
    1.53 -
    1.54 -  private val process =
    1.55 -    try {
    1.56 -      val cmdline = command_line(system_channel, prover_args)
    1.57 -      new Isabelle_System.Managed_Process(null, null, false, cmdline: _*)
    1.58 -    }
    1.59 -    catch { case e: IOException => system_channel.accepted(); throw(e) }
    1.60 -
    1.61    private val (_, process_result) =
    1.62 -    Simple_Thread.future("process_result") { process.join }
    1.63 +    Simple_Thread.future("process_result") { system_process.join }
    1.64  
    1.65    private def terminate_process()
    1.66    {
    1.67 -    try { process.terminate }
    1.68 -    catch { case e: IOException => system_output("Failed to terminate Isabelle: " + e.getMessage) }
    1.69 +    try { system_process.terminate }
    1.70 +    catch {
    1.71 +      case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage)
    1.72 +    }
    1.73    }
    1.74  
    1.75    private val process_manager = Simple_Thread.fork("process_manager")
    1.76 @@ -80,10 +89,10 @@
    1.77      {
    1.78        var finished: Option[Boolean] = None
    1.79        val result = new StringBuilder(100)
    1.80 -      while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) {
    1.81 -        while (finished.isEmpty && process.stderr.ready) {
    1.82 +      while (finished.isEmpty && (system_process.stderr.ready || !process_result.is_finished)) {
    1.83 +        while (finished.isEmpty && system_process.stderr.ready) {
    1.84            try {
    1.85 -            val c = process.stderr.read
    1.86 +            val c = system_process.stderr.read
    1.87              if (c == 2) finished = Some(true)
    1.88              else result += c.toChar
    1.89            }
    1.90 @@ -95,14 +104,13 @@
    1.91      }
    1.92      if (startup_errors != "") system_output(startup_errors)
    1.93  
    1.94 -    process.stdin.close
    1.95      if (startup_failed) {
    1.96        terminate_process()
    1.97        process_result.join
    1.98        exit_message(127)
    1.99      }
   1.100      else {
   1.101 -      val (command_stream, message_stream) = system_channel.rendezvous()
   1.102 +      val (command_stream, message_stream) = system_process.channel.rendezvous()
   1.103  
   1.104        command_input_init(command_stream)
   1.105        val stdout = physical_output(false)
   1.106 @@ -116,7 +124,7 @@
   1.107        system_output("process_manager terminated")
   1.108        exit_message(rc)
   1.109      }
   1.110 -    system_channel.accepted()
   1.111 +    system_process.channel.accepted()
   1.112    }
   1.113  
   1.114  
   1.115 @@ -124,16 +132,10 @@
   1.116  
   1.117    def join() { process_manager.join() }
   1.118  
   1.119 -  def interrupt()
   1.120 -  {
   1.121 -    try { process.interrupt }
   1.122 -    catch { case e: IOException => system_output("Failed to interrupt Isabelle: " + e.getMessage) }
   1.123 -  }
   1.124 -
   1.125    def terminate()
   1.126    {
   1.127      command_input_close()
   1.128 -    system_output("Terminating Isabelle process")
   1.129 +    system_output("Terminating prover process")
   1.130      terminate_process()
   1.131    }
   1.132  
   1.133 @@ -176,8 +178,8 @@
   1.134    private def physical_output(err: Boolean): Thread =
   1.135    {
   1.136      val (name, reader, markup) =
   1.137 -      if (err) ("standard_error", process.stderr, Markup.STDERR)
   1.138 -      else ("standard_output", process.stdout, Markup.STDOUT)
   1.139 +      if (err) ("standard_error", system_process.stderr, Markup.STDERR)
   1.140 +      else ("standard_output", system_process.stdout, Markup.STDOUT)
   1.141  
   1.142      Simple_Thread.fork(name) {
   1.143        try {