src/Pure/PIDE/query_operation.scala
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 57612 990ffb84489b
     1.1 --- a/src/Pure/PIDE/query_operation.scala	Fri Apr 25 12:27:18 2014 +0200
     1.2 +++ b/src/Pure/PIDE/query_operation.scala	Fri Apr 25 12:51:08 2014 +0200
     1.3 @@ -8,9 +8,6 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import scala.actors.Actor._
     1.8 -
     1.9 -
    1.10  object Query_Operation
    1.11  {
    1.12    object Status extends Enumeration
    1.13 @@ -33,12 +30,12 @@
    1.14  
    1.15    /* implicit state -- owned by Swing thread */
    1.16  
    1.17 -  private var current_location: Option[Command] = None
    1.18 -  private var current_query: List[String] = Nil
    1.19 -  private var current_update_pending = false
    1.20 -  private var current_output: List[XML.Tree] = Nil
    1.21 -  private var current_status = Query_Operation.Status.FINISHED
    1.22 -  private var current_exec_id = Document_ID.none
    1.23 +  @volatile private var current_location: Option[Command] = None
    1.24 +  @volatile private var current_query: List[String] = Nil
    1.25 +  @volatile private var current_update_pending = false
    1.26 +  @volatile private var current_output: List[XML.Tree] = Nil
    1.27 +  @volatile private var current_status = Query_Operation.Status.FINISHED
    1.28 +  @volatile private var current_exec_id = Document_ID.none
    1.29  
    1.30    private def reset_state()
    1.31    {
    1.32 @@ -209,32 +206,27 @@
    1.33    }
    1.34  
    1.35  
    1.36 -  /* main actor */
    1.37 +  /* main */
    1.38  
    1.39 -  private val main_actor = actor {
    1.40 -    loop {
    1.41 -      react {
    1.42 -        case changed: Session.Commands_Changed =>
    1.43 -          current_location match {
    1.44 -            case Some(command)
    1.45 -            if current_update_pending ||
    1.46 -              (current_status != Query_Operation.Status.FINISHED &&
    1.47 -                changed.commands.contains(command)) =>
    1.48 -              Swing_Thread.later { content_update() }
    1.49 -            case _ =>
    1.50 -          }
    1.51 -        case bad =>
    1.52 -          System.err.println("Query_Operation: ignoring bad message " + bad)
    1.53 -      }
    1.54 +  private val main =
    1.55 +    Session.Consumer[Session.Commands_Changed](getClass.getName) {
    1.56 +      case changed =>
    1.57 +        current_location match {
    1.58 +          case Some(command)
    1.59 +          if current_update_pending ||
    1.60 +            (current_status != Query_Operation.Status.FINISHED &&
    1.61 +              changed.commands.contains(command)) =>
    1.62 +            Swing_Thread.later { content_update() }
    1.63 +          case _ =>
    1.64 +        }
    1.65      }
    1.66 -  }
    1.67  
    1.68    def activate() {
    1.69 -    editor.session.commands_changed += main_actor
    1.70 +    editor.session.commands_changed += main
    1.71    }
    1.72  
    1.73    def deactivate() {
    1.74 -    editor.session.commands_changed -= main_actor
    1.75 +    editor.session.commands_changed -= main
    1.76      remove_overlay()
    1.77      reset_state()
    1.78      consume_output(Document.Snapshot.init, Command.Results.empty, Nil)