--- a/src/Pure/Concurrent/simple_thread.scala Wed Sep 22 13:47:48 2010 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala Wed Sep 22 14:06:48 2010 +0200
@@ -26,8 +26,6 @@
thread
}
- def fork(body: => Unit): Thread = fork()(body)
-
/* future result via thread */
@@ -38,8 +36,6 @@
result
}
- def future[A](body: => A): Future[A] = future()(body)
-
/* thread as actor */
--- a/src/Pure/System/isabelle_system.scala Wed Sep 22 13:47:48 2010 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Sep 22 14:06:48 2010 +0200
@@ -273,8 +273,8 @@
val proc = new Managed_Process(false, "bash", posix_path(script_file.getPath))
proc.stdin.close
- val stdout = Simple_Thread.future { Standard_System.slurp(proc.stdout) }
- val stderr = Simple_Thread.future { Standard_System.slurp(proc.stderr) }
+ val stdout = Simple_Thread.future("bash_stdout") { Standard_System.slurp(proc.stdout) }
+ val stderr = Simple_Thread.future("bash_stderr") { Standard_System.slurp(proc.stderr) }
val rc =
try { proc.join }