reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
authorwenzelm
Thu Apr 17 14:52:23 2014 +0200 (2014-04-17)
changeset 56617c00646996701
parent 56616 abc2da18d08d
child 56618 874bdedb2313
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);
src/Pure/System/isabelle_process.scala
     1.1 --- a/src/Pure/System/isabelle_process.scala	Thu Apr 17 13:21:36 2014 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Thu Apr 17 14:52:23 2014 +0200
     1.3 @@ -147,6 +147,12 @@
     1.4  
     1.5    def join() { process_manager.join() }
     1.6  
     1.7 +  def interrupt()
     1.8 +  {
     1.9 +    try { process.interrupt }
    1.10 +    catch { case e: IOException => system_output("Failed to interrupt Isabelle: " + e.getMessage) }
    1.11 +  }
    1.12 +
    1.13    def terminate()
    1.14    {
    1.15      close(command_input)