# HG changeset patch
# User wenzelm
# Date 1285157208 -7200
# Node ID ea8f3ea13a9514d23a5fd3817b727b6f8ce1cc53
# Parent  00be8711082f4826981b50070cb4fb93308e7e4c
eliminated Simple_Thread shorthands that can overlap with full version;

diff -r 00be8711082f -r ea8f3ea13a95 src/Pure/Concurrent/simple_thread.scala
--- 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 */
 
diff -r 00be8711082f -r ea8f3ea13a95 src/Pure/System/isabelle_system.scala
--- 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 }