# HG changeset patch
# User wenzelm
# Date 1282572438 -7200
# Node ID b7647ca7de5ac1486530bfb91b615b5383b698d0
# Parent  f76ad0771f67b19469faddb5f07e4cd8c9159f10
module for simplified thread operations (Scala version);

diff -r f76ad0771f67 -r b7647ca7de5a src/Pure/Concurrent/simple_thread.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/simple_thread.scala	Mon Aug 23 16:07:18 2010 +0200
@@ -0,0 +1,36 @@
+/*  Title:      Pure/Concurrent/simple_thread.scala
+    Author:     Makarius
+
+Simplified thread operations.
+*/
+
+package isabelle
+
+
+import java.lang.Thread
+
+import scala.actors.Actor
+
+
+object Simple_Thread
+{
+  /* plain thread */
+
+  def fork(name: String)(body: => Unit): Thread =
+  {
+    val thread = new Thread(name) { override def run = body }
+    thread.start
+    thread
+  }
+
+
+  /* thread as actor */
+
+  def actor(name: String)(body: => Unit): Actor =
+  {
+    val actor = Future.promise[Actor]
+    val thread = fork(name) { actor.fulfill(Actor.self); body }
+    actor.join
+  }
+}
+
diff -r f76ad0771f67 -r b7647ca7de5a src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Aug 23 15:11:41 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Aug 23 16:07:18 2010 +0200
@@ -155,7 +155,7 @@
   /* raw stdin */
 
   private def stdin_actor(name: String, stream: OutputStream): Actor =
-    Library.thread_actor(name) {
+    Simple_Thread.actor(name) {
       val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset))
       var finished = false
       while (!finished) {
@@ -184,7 +184,7 @@
   /* raw stdout */
 
   private def stdout_actor(name: String, stream: InputStream): Actor =
-    Library.thread_actor(name) {
+    Simple_Thread.actor(name) {
       val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
       var result = new StringBuilder(100)
 
@@ -221,7 +221,7 @@
   /* command input */
 
   private def input_actor(name: String, raw_stream: OutputStream): Actor =
-    Library.thread_actor(name) {
+    Simple_Thread.actor(name) {
       val stream = new BufferedOutputStream(raw_stream)
       var finished = false
       while (!finished) {
@@ -253,7 +253,7 @@
   private class Protocol_Error(msg: String) extends Exception(msg)
 
   private def message_actor(name: String, stream: InputStream): Actor =
-    Library.thread_actor(name) {
+    Simple_Thread.actor(name) {
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
@@ -344,7 +344,7 @@
 
   /* exit process */
 
-  Library.thread_actor("process_exit") {
+  Simple_Thread.actor("process_exit") {
     proc match {
       case None =>
       case Some(p) =>
diff -r f76ad0771f67 -r b7647ca7de5a src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Aug 23 15:11:41 2010 +0200
+++ b/src/Pure/build-jars	Mon Aug 23 16:07:18 2010 +0200
@@ -23,6 +23,7 @@
 
 declare -a SOURCES=(
   Concurrent/future.scala
+  Concurrent/simple_thread.scala
   General/exn.scala
   General/linear_set.scala
   General/markup.scala
diff -r f76ad0771f67 -r b7647ca7de5a src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Aug 23 15:11:41 2010 +0200
+++ b/src/Pure/library.scala	Mon Aug 23 16:07:18 2010 +0200
@@ -7,11 +7,10 @@
 package isabelle
 
 
-import java.lang.{System, Thread}
+import java.lang.System
 import java.awt.Component
 import javax.swing.JOptionPane
 
-import scala.actors.Actor
 import scala.swing.ComboBox
 import scala.swing.event.SelectionChanged
 
@@ -139,15 +138,4 @@
         ((stop - start).toDouble / 1000000) + "ms elapsed time")
     Exn.release(result)
   }
-
-
-  /* thread as actor */
-
-  def thread_actor(name: String)(body: => Unit): Actor =
-  {
-    val actor = Future.promise[Actor]
-    val thread = new Thread(name) { override def run() = { actor.fulfill(Actor.self); body } }
-    thread.start
-    actor.join
-  }
 }