# HG changeset patch
# User wenzelm
# Date 1397739143 -7200
# Node ID c006469967016e7d24e0fddfce961d69ec1608a7
# Parent  abc2da18d08db9617eebc9596b192b9aa50efb7a
reintroduced process interrupt for the sake of synchronous protocol commands like "use_theories" (see also 27930cf6f0f7);

diff -r abc2da18d08d -r c00646996701 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Thu Apr 17 13:21:36 2014 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu Apr 17 14:52:23 2014 +0200
@@ -147,6 +147,12 @@
 
   def join() { process_manager.join() }
 
+  def interrupt()
+  {
+    try { process.interrupt }
+    catch { case e: IOException => system_output("Failed to interrupt Isabelle: " + e.getMessage) }
+  }
+
   def terminate()
   {
     close(command_input)