simplified -- prefer Consumer_Thread over Actor;
authorwenzelm
Thu Apr 24 16:52:17 2014 +0200 (2014-04-24)
changeset 56704c2f0ddd14747
parent 56703 2d0ca179e749
child 56705 937826d702d5
simplified -- prefer Consumer_Thread over Actor;
src/Pure/Concurrent/simple_thread.scala
src/Pure/PIDE/session.scala
     1.1 --- a/src/Pure/Concurrent/simple_thread.scala	Thu Apr 24 16:47:47 2014 +0200
     1.2 +++ b/src/Pure/Concurrent/simple_thread.scala	Thu Apr 24 16:52:17 2014 +0200
     1.3 @@ -46,11 +46,11 @@
     1.4  
     1.5    /* thread as actor */
     1.6  
     1.7 -  def actor(name: String, daemon: Boolean = false)(body: => Unit): (Thread, Actor) =
     1.8 +  def actor(name: String, daemon: Boolean = false)(body: => Unit): Actor =
     1.9    {
    1.10      val actor = Future.promise[Actor]
    1.11      val thread = fork(name, daemon) { actor.fulfill(Actor.self); body }
    1.12 -    (thread, actor.join)
    1.13 +    actor.join
    1.14    }
    1.15  }
    1.16  
     2.1 --- a/src/Pure/PIDE/session.scala	Thu Apr 24 16:47:47 2014 +0200
     2.2 +++ b/src/Pure/PIDE/session.scala	Thu Apr 24 16:52:17 2014 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4  
     2.5  import scala.collection.mutable
     2.6  import scala.collection.immutable.Queue
     2.7 -import scala.actors.TIMEOUT
     2.8 +import scala.actors.{Actor, TIMEOUT}
     2.9  import scala.actors.Actor._
    2.10  
    2.11  
    2.12 @@ -152,54 +152,33 @@
    2.13  
    2.14    /** buffered command changes (delay_first discipline) **/
    2.15  
    2.16 -  //{{{
    2.17 -  private case object Stop
    2.18 -
    2.19 -  private val (_, commands_changed_buffer) =
    2.20 -    Simple_Thread.actor("commands_changed_buffer", daemon = true)
    2.21 +  private val commands_changed_buffer =
    2.22 +    Consumer_Thread.fork[Session.Commands_Changed]("commands_changed_buffer", daemon = true)
    2.23    {
    2.24 -    var finished = false
    2.25 -    while (!finished) {
    2.26 -      receive {
    2.27 -        case Stop => finished = true; reply(())
    2.28 -        case changed: Session.Commands_Changed => commands_changed.event(changed)
    2.29 -        case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
    2.30 -      }
    2.31 -    }
    2.32 +    case changed => commands_changed.event(changed); true
    2.33    }
    2.34 -  //}}}
    2.35  
    2.36  
    2.37    /** pipelined change parsing **/
    2.38  
    2.39 -  //{{{
    2.40    private case class Text_Edits(
    2.41      previous: Future[Document.Version],
    2.42      doc_blobs: Document.Blobs,
    2.43      text_edits: List[Document.Edit_Text],
    2.44      version_result: Promise[Document.Version])
    2.45  
    2.46 -  private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true)
    2.47 +  private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
    2.48    {
    2.49 -    var finished = false
    2.50 -    while (!finished) {
    2.51 -      receive {
    2.52 -        case Stop => finished = true; reply(())
    2.53 -
    2.54 -        case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
    2.55 -          val prev = previous.get_finished
    2.56 -          val change =
    2.57 -            Timing.timeit("parse_change", timing) {
    2.58 -              resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
    2.59 -            }
    2.60 -          version_result.fulfill(change.version)
    2.61 -          sender ! change
    2.62 -
    2.63 -        case bad => System.err.println("change_parser: ignoring bad message " + bad)
    2.64 -      }
    2.65 -    }
    2.66 +    case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
    2.67 +      val prev = previous.get_finished
    2.68 +      val change =
    2.69 +        Timing.timeit("parse_change", timing) {
    2.70 +          resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
    2.71 +        }
    2.72 +      version_result.fulfill(change.version)
    2.73 +      session_actor ! change
    2.74 +      true
    2.75    }
    2.76 -  //}}}
    2.77  
    2.78  
    2.79  
    2.80 @@ -255,13 +234,14 @@
    2.81  
    2.82    /* actor messages */
    2.83  
    2.84 +  private case object Stop
    2.85    private case class Start(name: String, args: List[String])
    2.86    private case class Cancel_Exec(exec_id: Document_ID.Exec)
    2.87    private case class Protocol_Command(name: String, args: List[String])
    2.88    private case class Messages(msgs: List[Prover.Message])
    2.89    private case class Update_Options(options: Options)
    2.90  
    2.91 -  private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
    2.92 +  private val session_actor: Actor = Simple_Thread.actor("session_actor", daemon = true)
    2.93    {
    2.94      val this_actor = self
    2.95  
    2.96 @@ -326,8 +306,8 @@
    2.97        def flush()
    2.98        {
    2.99          if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty)
   2.100 -          commands_changed_buffer !
   2.101 -            Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands)
   2.102 +          commands_changed_buffer.send(
   2.103 +            Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands))
   2.104          changed_assignment = false
   2.105          changed_nodes = Set.empty
   2.106          changed_commands = Set.empty
   2.107 @@ -362,7 +342,7 @@
   2.108        val change = global_state.change_result(_.continue_history(previous, edits, version))
   2.109  
   2.110        raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
   2.111 -      change_parser ! Text_Edits(previous, doc_blobs, edits, version)
   2.112 +      change_parser.send(Text_Edits(previous, doc_blobs, edits, version))
   2.113      }
   2.114      //}}}
   2.115  
   2.116 @@ -576,8 +556,8 @@
   2.117  
   2.118    def stop()
   2.119    {
   2.120 -    commands_changed_buffer !? Stop
   2.121 -    change_parser !? Stop
   2.122 +    commands_changed_buffer.shutdown()
   2.123 +    change_parser.shutdown()
   2.124      session_actor !? Stop
   2.125    }
   2.126