src/Pure/PIDE/session.scala
changeset 56704 c2f0ddd14747
parent 56691 ad5d7461b370
child 56705 937826d702d5
     1.1 --- a/src/Pure/PIDE/session.scala	Thu Apr 24 16:47:47 2014 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Thu Apr 24 16:52:17 2014 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  import scala.collection.mutable
     1.6  import scala.collection.immutable.Queue
     1.7 -import scala.actors.TIMEOUT
     1.8 +import scala.actors.{Actor, TIMEOUT}
     1.9  import scala.actors.Actor._
    1.10  
    1.11  
    1.12 @@ -152,54 +152,33 @@
    1.13  
    1.14    /** buffered command changes (delay_first discipline) **/
    1.15  
    1.16 -  //{{{
    1.17 -  private case object Stop
    1.18 -
    1.19 -  private val (_, commands_changed_buffer) =
    1.20 -    Simple_Thread.actor("commands_changed_buffer", daemon = true)
    1.21 +  private val commands_changed_buffer =
    1.22 +    Consumer_Thread.fork[Session.Commands_Changed]("commands_changed_buffer", daemon = true)
    1.23    {
    1.24 -    var finished = false
    1.25 -    while (!finished) {
    1.26 -      receive {
    1.27 -        case Stop => finished = true; reply(())
    1.28 -        case changed: Session.Commands_Changed => commands_changed.event(changed)
    1.29 -        case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
    1.30 -      }
    1.31 -    }
    1.32 +    case changed => commands_changed.event(changed); true
    1.33    }
    1.34 -  //}}}
    1.35  
    1.36  
    1.37    /** pipelined change parsing **/
    1.38  
    1.39 -  //{{{
    1.40    private case class Text_Edits(
    1.41      previous: Future[Document.Version],
    1.42      doc_blobs: Document.Blobs,
    1.43      text_edits: List[Document.Edit_Text],
    1.44      version_result: Promise[Document.Version])
    1.45  
    1.46 -  private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true)
    1.47 +  private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true)
    1.48    {
    1.49 -    var finished = false
    1.50 -    while (!finished) {
    1.51 -      receive {
    1.52 -        case Stop => finished = true; reply(())
    1.53 -
    1.54 -        case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
    1.55 -          val prev = previous.get_finished
    1.56 -          val change =
    1.57 -            Timing.timeit("parse_change", timing) {
    1.58 -              resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
    1.59 -            }
    1.60 -          version_result.fulfill(change.version)
    1.61 -          sender ! change
    1.62 -
    1.63 -        case bad => System.err.println("change_parser: ignoring bad message " + bad)
    1.64 -      }
    1.65 -    }
    1.66 +    case Text_Edits(previous, doc_blobs, text_edits, version_result) =>
    1.67 +      val prev = previous.get_finished
    1.68 +      val change =
    1.69 +        Timing.timeit("parse_change", timing) {
    1.70 +          resources.parse_change(reparse_limit, prev, doc_blobs, text_edits)
    1.71 +        }
    1.72 +      version_result.fulfill(change.version)
    1.73 +      session_actor ! change
    1.74 +      true
    1.75    }
    1.76 -  //}}}
    1.77  
    1.78  
    1.79  
    1.80 @@ -255,13 +234,14 @@
    1.81  
    1.82    /* actor messages */
    1.83  
    1.84 +  private case object Stop
    1.85    private case class Start(name: String, args: List[String])
    1.86    private case class Cancel_Exec(exec_id: Document_ID.Exec)
    1.87    private case class Protocol_Command(name: String, args: List[String])
    1.88    private case class Messages(msgs: List[Prover.Message])
    1.89    private case class Update_Options(options: Options)
    1.90  
    1.91 -  private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
    1.92 +  private val session_actor: Actor = Simple_Thread.actor("session_actor", daemon = true)
    1.93    {
    1.94      val this_actor = self
    1.95  
    1.96 @@ -326,8 +306,8 @@
    1.97        def flush()
    1.98        {
    1.99          if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty)
   1.100 -          commands_changed_buffer !
   1.101 -            Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands)
   1.102 +          commands_changed_buffer.send(
   1.103 +            Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands))
   1.104          changed_assignment = false
   1.105          changed_nodes = Set.empty
   1.106          changed_commands = Set.empty
   1.107 @@ -362,7 +342,7 @@
   1.108        val change = global_state.change_result(_.continue_history(previous, edits, version))
   1.109  
   1.110        raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
   1.111 -      change_parser ! Text_Edits(previous, doc_blobs, edits, version)
   1.112 +      change_parser.send(Text_Edits(previous, doc_blobs, edits, version))
   1.113      }
   1.114      //}}}
   1.115  
   1.116 @@ -576,8 +556,8 @@
   1.117  
   1.118    def stop()
   1.119    {
   1.120 -    commands_changed_buffer !? Stop
   1.121 -    change_parser !? Stop
   1.122 +    commands_changed_buffer.shutdown()
   1.123 +    change_parser.shutdown()
   1.124      session_actor !? Stop
   1.125    }
   1.126