eliminated Simple_Thread shorthands that can overlap with full version;
authorwenzelm
Wed, 22 Sep 2010 14:06:48 +0200
changeset 39586 ea8f3ea13a95
parent 39585 00be8711082f
child 39587 f84b70e3bb9c
eliminated Simple_Thread shorthands that can overlap with full version;
src/Pure/Concurrent/simple_thread.scala
src/Pure/System/isabelle_system.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 */
 
--- 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 }