1.1 --- a/src/Pure/System/isabelle_process.scala	Mon Aug 23 15:11:41 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Mon Aug 23 16:07:18 2010 +0200
     1.3 @@ -155,7 +155,7 @@
     1.4    /* raw stdin */
     1.5  
     1.6    private def stdin_actor(name: String, stream: OutputStream): Actor =
     1.7 -    Library.thread_actor(name) {
     1.8 +    Simple_Thread.actor(name) {
     1.9        val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset))
    1.10        var finished = false
    1.11        while (!finished) {
    1.12 @@ -184,7 +184,7 @@
    1.13    /* raw stdout */
    1.14  
    1.15    private def stdout_actor(name: String, stream: InputStream): Actor =
    1.16 -    Library.thread_actor(name) {
    1.17 +    Simple_Thread.actor(name) {
    1.18        val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
    1.19        var result = new StringBuilder(100)
    1.20  
    1.21 @@ -221,7 +221,7 @@
    1.22    /* command input */
    1.23  
    1.24    private def input_actor(name: String, raw_stream: OutputStream): Actor =
    1.25 -    Library.thread_actor(name) {
    1.26 +    Simple_Thread.actor(name) {
    1.27        val stream = new BufferedOutputStream(raw_stream)
    1.28        var finished = false
    1.29        while (!finished) {
    1.30 @@ -253,7 +253,7 @@
    1.31    private class Protocol_Error(msg: String) extends Exception(msg)
    1.32  
    1.33    private def message_actor(name: String, stream: InputStream): Actor =
    1.34 -    Library.thread_actor(name) {
    1.35 +    Simple_Thread.actor(name) {
    1.36        val default_buffer = new Array[Byte](65536)
    1.37        var c = -1
    1.38  
    1.39 @@ -344,7 +344,7 @@
    1.40  
    1.41    /* exit process */
    1.42  
    1.43 -  Library.thread_actor("process_exit") {
    1.44 +  Simple_Thread.actor("process_exit") {
    1.45      proc match {
    1.46        case None =>
    1.47        case Some(p) =>