# HG changeset patch
# User wenzelm
# Date 1457461796 -3600
# Node ID 4bf00f54e4bc5d07b1a6fc50d12ca48083dce3fd
# Parent  498f6ff1680416a6d2680698a22b6ac9da0604a6
ignore execeptions that usually occur due to shutdown;

diff -r 498f6ff16804 -r 4bf00f54e4bc src/Pure/Tools/ml_console.scala
--- a/src/Pure/Tools/ml_console.scala	Tue Mar 08 18:38:29 2016 +0100
+++ b/src/Pure/Tools/ml_console.scala	Tue Mar 08 19:29:56 2016 +0100
@@ -7,6 +7,8 @@
 package isabelle
 
 
+import java.io.IOException
+
 import scala.annotation.tailrec
 
 import jline.console.ConsoleReader
@@ -78,41 +80,47 @@
         ML_Process(options, heap = logic,
           modes = if (logic == "RAW_ML_SYSTEM") Nil else modes ::: List("ASCII"))
       val process_output = Future.thread[Unit]("process_output") {
-        var result = new StringBuilder(100)
-        var finished = false
-        while (!finished) {
-          var c = -1
-          var done = false
-          while (!done && (result.length == 0 || process.stdout.ready)) {
-            c = process.stdout.read
-            if (c >= 0) result.append(c.asInstanceOf[Char])
-            else done = true
-          }
-          if (result.length > 0) {
-            System.out.print(result.toString)
-            System.out.flush()
-            result.length = 0
-          }
-          else {
-            process.stdout.close()
-            finished = true
+        try {
+          var result = new StringBuilder(100)
+          var finished = false
+          while (!finished) {
+            var c = -1
+            var done = false
+            while (!done && (result.length == 0 || process.stdout.ready)) {
+              c = process.stdout.read
+              if (c >= 0) result.append(c.asInstanceOf[Char])
+              else done = true
+            }
+            if (result.length > 0) {
+              System.out.print(result.toString)
+              System.out.flush()
+              result.length = 0
+            }
+            else {
+              process.stdout.close()
+              finished = true
+            }
           }
         }
+        catch { case e: IOException => case Exn.Interrupt() => }
       }
       val process_input = Future.thread[Unit]("process_input") {
         POSIX_Interrupt.handler { process.interrupt } {
-          var finished = false
-          while (!finished) {
-            reader.readLine() match {
-              case null =>
-                process.stdin.close()
-                finished = true
-              case line =>
-                process.stdin.write(line)
-                process.stdin.write("\n")
-                process.stdin.flush()
+          try {
+            var finished = false
+            while (!finished) {
+              reader.readLine() match {
+                case null =>
+                  process.stdin.close()
+                  finished = true
+                case line =>
+                  process.stdin.write(line)
+                  process.stdin.write("\n")
+                  process.stdin.flush()
+              }
             }
           }
+          catch { case e: IOException => case Exn.Interrupt() => }
         }
       }
       val process_result = Future.thread[Int]("process_result") {