clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
authorwenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 5671552125652e82a
parent 56714 061f83259922
child 56716 6d5733303a50
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
src/Pure/PIDE/query_operation.scala
src/Pure/PIDE/session.scala
src/Pure/Tools/simplifier_trace.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/find_dockable.scala
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/monitor_dockable.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/protocol_dockable.scala
src/Tools/jEdit/src/raw_output_dockable.scala
src/Tools/jEdit/src/simplifier_trace_dockable.scala
src/Tools/jEdit/src/sledgehammer_dockable.scala
src/Tools/jEdit/src/syslog_dockable.scala
src/Tools/jEdit/src/theories_dockable.scala
src/Tools/jEdit/src/timing_dockable.scala
     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)
     2.1 --- a/src/Pure/PIDE/session.scala	Fri Apr 25 12:27:18 2014 +0200
     2.2 +++ b/src/Pure/PIDE/session.scala	Fri Apr 25 12:51:08 2014 +0200
     2.3 @@ -16,6 +16,36 @@
     2.4  
     2.5  object Session
     2.6  {
     2.7 +  /* outlets */
     2.8 +
     2.9 +  object Consumer
    2.10 +  {
    2.11 +    def apply[A](name: String)(consume: A => Unit): Consumer[A] =
    2.12 +      new Consumer[A](name, consume)
    2.13 +  }
    2.14 +  final class Consumer[-A] private(val name: String, val consume: A => Unit)
    2.15 +
    2.16 +  class Outlet[A](dispatcher: Consumer_Thread[() => Unit])
    2.17 +  {
    2.18 +    private val consumers = Synchronized(List.empty[Consumer[A]])
    2.19 +
    2.20 +    def += (c: Consumer[A]) { consumers.change(Library.update(c)) }
    2.21 +    def -= (c: Consumer[A]) { consumers.change(Library.remove(c)) }
    2.22 +
    2.23 +    def post(a: A)
    2.24 +    {
    2.25 +      for (c <- consumers.value.iterator) {
    2.26 +        dispatcher.send(() =>
    2.27 +          try { c.consume(a) }
    2.28 +          catch {
    2.29 +            case exn: Throwable =>
    2.30 +              System.err.println("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
    2.31 +          })
    2.32 +      }
    2.33 +    }
    2.34 +  }
    2.35 +
    2.36 +
    2.37    /* change */
    2.38  
    2.39    sealed case class Change(
    2.40 @@ -134,18 +164,21 @@
    2.41    def reparse_limit: Int = 0
    2.42  
    2.43  
    2.44 -  /* pervasive event buses */
    2.45 +  /* outlets */
    2.46 +
    2.47 +  private val dispatcher =
    2.48 +    Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true }
    2.49  
    2.50 -  val statistics = new Event_Bus[Session.Statistics]
    2.51 -  val global_options = new Event_Bus[Session.Global_Options]
    2.52 -  val caret_focus = new Event_Bus[Session.Caret_Focus.type]
    2.53 -  val raw_edits = new Event_Bus[Session.Raw_Edits]
    2.54 -  val commands_changed = new Event_Bus[Session.Commands_Changed]
    2.55 -  val phase_changed = new Event_Bus[Session.Phase]
    2.56 -  val syslog_messages = new Event_Bus[Prover.Output]
    2.57 -  val raw_output_messages = new Event_Bus[Prover.Output]
    2.58 -  val all_messages = new Event_Bus[Prover.Message]  // potential bottle-neck
    2.59 -  val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
    2.60 +  val statistics = new Session.Outlet[Session.Statistics](dispatcher)
    2.61 +  val global_options = new Session.Outlet[Session.Global_Options](dispatcher)
    2.62 +  val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher)
    2.63 +  val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher)
    2.64 +  val commands_changed = new Session.Outlet[Session.Commands_Changed](dispatcher)
    2.65 +  val phase_changed = new Session.Outlet[Session.Phase](dispatcher)
    2.66 +  val syslog_messages = new Session.Outlet[Prover.Output](dispatcher)
    2.67 +  val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher)
    2.68 +  val all_messages = new Session.Outlet[Prover.Message](dispatcher)  // potential bottle-neck
    2.69 +  val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher)
    2.70  
    2.71  
    2.72  
    2.73 @@ -163,7 +196,7 @@
    2.74  
    2.75        def flush(): Unit = synchronized {
    2.76          if (assignment || !nodes.isEmpty || !commands.isEmpty)
    2.77 -          commands_changed.event(Session.Commands_Changed(assignment, nodes, commands))
    2.78 +          commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
    2.79          assignment = false
    2.80          nodes = Set.empty
    2.81          commands = Set.empty
    2.82 @@ -223,7 +256,7 @@
    2.83    private def phase_=(new_phase: Session.Phase)
    2.84    {
    2.85      _phase = new_phase
    2.86 -    phase_changed.event(new_phase)
    2.87 +    phase_changed.post(new_phase)
    2.88    }
    2.89    def phase = _phase
    2.90    def is_ready: Boolean = phase == Session.Ready
    2.91 @@ -349,7 +382,7 @@
    2.92        val version = Future.promise[Document.Version]
    2.93        global_state.change(_.continue_history(previous, edits, version))
    2.94  
    2.95 -      raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
    2.96 +      raw_edits.post(Session.Raw_Edits(doc_blobs, edits))
    2.97        change_parser.send(Text_Edits(previous, doc_blobs, edits, version))
    2.98      }
    2.99      //}}}
   2.100 @@ -458,7 +491,7 @@
   2.101                  }
   2.102  
   2.103                case Markup.ML_Statistics(props) =>
   2.104 -                statistics.event(Session.Statistics(props))
   2.105 +                statistics.post(Session.Statistics(props))
   2.106  
   2.107                case Markup.Task_Statistics(props) =>
   2.108                  // FIXME
   2.109 @@ -479,7 +512,7 @@
   2.110                if (rc == 0) phase = Session.Inactive
   2.111                else phase = Session.Failed
   2.112  
   2.113 -            case _ => raw_output_messages.event(output)
   2.114 +            case _ => raw_output_messages.post(output)
   2.115            }
   2.116          }
   2.117      }
   2.118 @@ -512,7 +545,7 @@
   2.119                prover.get.options(options)
   2.120                handle_raw_edits(Document.Blobs.empty, Nil)
   2.121              }
   2.122 -            global_options.event(Session.Global_Options(options))
   2.123 +            global_options.post(Session.Global_Options(options))
   2.124  
   2.125            case Cancel_Exec(exec_id) if prover.isDefined =>
   2.126              prover.get.cancel_exec(exec_id)
   2.127 @@ -530,13 +563,13 @@
   2.128            case Messages(msgs) =>
   2.129              msgs foreach {
   2.130                case input: Prover.Input =>
   2.131 -                all_messages.event(input)
   2.132 +                all_messages.post(input)
   2.133  
   2.134                case output: Prover.Output =>
   2.135 -                if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
   2.136 +                if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
   2.137                  else handle_output(output)
   2.138 -                if (output.is_syslog) syslog_messages.event(output)
   2.139 -                all_messages.event(output)
   2.140 +                if (output.is_syslog) syslog_messages.post(output)
   2.141 +                all_messages.post(output)
   2.142              }
   2.143  
   2.144            case change: Session.Change if prover.isDefined =>
   2.145 @@ -562,6 +595,7 @@
   2.146      change_parser.shutdown()
   2.147      change_buffer.shutdown()
   2.148      manager.shutdown()
   2.149 +    dispatcher.shutdown()
   2.150    }
   2.151  
   2.152    def protocol_command(name: String, args: String*)
     3.1 --- a/src/Pure/Tools/simplifier_trace.scala	Fri Apr 25 12:27:18 2014 +0200
     3.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Fri Apr 25 12:51:08 2014 +0200
     3.3 @@ -287,7 +287,7 @@
     3.4            }
     3.5  
     3.6            do_reply(session, serial, answer)
     3.7 -          session.trace_events.event(Event)
     3.8 +          session.trace_events.post(Event)
     3.9  
    3.10          case bad =>
    3.11            System.err.println("context_manager: bad message " + bad)
     4.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Apr 25 12:27:18 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Apr 25 12:51:08 2014 +0200
     4.3 @@ -10,8 +10,6 @@
     4.4  
     4.5  import isabelle._
     4.6  
     4.7 -import scala.actors.Actor._
     4.8 -
     4.9  import java.awt.Graphics2D
    4.10  import java.awt.event.KeyEvent
    4.11  import javax.swing.event.{CaretListener, CaretEvent}
    4.12 @@ -176,7 +174,7 @@
    4.13  
    4.14    private val delay_caret_update =
    4.15      Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
    4.16 -      session.caret_focus.event(Session.Caret_Focus)
    4.17 +      session.caret_focus.post(Session.Caret_Focus)
    4.18      }
    4.19  
    4.20    private val caret_listener = new CaretListener {
    4.21 @@ -193,60 +191,54 @@
    4.22    }
    4.23  
    4.24  
    4.25 -  /* main actor */
    4.26 +  /* main */
    4.27  
    4.28 -  private val main_actor = actor {
    4.29 -    loop {
    4.30 -      react {
    4.31 -        case _: Session.Raw_Edits =>
    4.32 -          Swing_Thread.later {
    4.33 -            overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
    4.34 -          }
    4.35 +  private val main =
    4.36 +    Session.Consumer[Any](getClass.getName) {
    4.37 +      case _: Session.Raw_Edits =>
    4.38 +        Swing_Thread.later {
    4.39 +          overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
    4.40 +        }
    4.41  
    4.42 -        case changed: Session.Commands_Changed =>
    4.43 -          val buffer = model.buffer
    4.44 -          Swing_Thread.later {
    4.45 -            JEdit_Lib.buffer_lock(buffer) {
    4.46 -              if (model.buffer == text_area.getBuffer) {
    4.47 -                val snapshot = model.snapshot()
    4.48 +      case changed: Session.Commands_Changed =>
    4.49 +        val buffer = model.buffer
    4.50 +        Swing_Thread.later {
    4.51 +          JEdit_Lib.buffer_lock(buffer) {
    4.52 +            if (model.buffer == text_area.getBuffer) {
    4.53 +              val snapshot = model.snapshot()
    4.54  
    4.55 -                val load_changed =
    4.56 -                  snapshot.load_commands.exists(changed.commands.contains)
    4.57 +              val load_changed =
    4.58 +                snapshot.load_commands.exists(changed.commands.contains)
    4.59  
    4.60 -                if (changed.assignment || load_changed ||
    4.61 -                    (changed.nodes.contains(model.node_name) &&
    4.62 -                     changed.commands.exists(snapshot.node.commands.contains)))
    4.63 -                  Swing_Thread.later { overview.delay_repaint.invoke() }
    4.64 +              if (changed.assignment || load_changed ||
    4.65 +                  (changed.nodes.contains(model.node_name) &&
    4.66 +                   changed.commands.exists(snapshot.node.commands.contains)))
    4.67 +                Swing_Thread.later { overview.delay_repaint.invoke() }
    4.68  
    4.69 -                val visible_lines = text_area.getVisibleLines
    4.70 -                if (visible_lines > 0) {
    4.71 -                  if (changed.assignment || load_changed)
    4.72 -                    text_area.invalidateScreenLineRange(0, visible_lines)
    4.73 -                  else {
    4.74 -                    val visible_range = JEdit_Lib.visible_range(text_area).get
    4.75 -                    val visible_iterator =
    4.76 -                      snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
    4.77 -                    if (visible_iterator.exists(changed.commands)) {
    4.78 -                      for {
    4.79 -                        line <- (0 until visible_lines).iterator
    4.80 -                        start = text_area.getScreenLineStartOffset(line) if start >= 0
    4.81 -                        end = text_area.getScreenLineEndOffset(line) if end >= 0
    4.82 -                        range = Text.Range(start, end)
    4.83 -                        line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
    4.84 -                        if line_cmds.exists(changed.commands)
    4.85 -                      } text_area.invalidateScreenLineRange(line, line)
    4.86 -                    }
    4.87 +              val visible_lines = text_area.getVisibleLines
    4.88 +              if (visible_lines > 0) {
    4.89 +                if (changed.assignment || load_changed)
    4.90 +                  text_area.invalidateScreenLineRange(0, visible_lines)
    4.91 +                else {
    4.92 +                  val visible_range = JEdit_Lib.visible_range(text_area).get
    4.93 +                  val visible_iterator =
    4.94 +                    snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
    4.95 +                  if (visible_iterator.exists(changed.commands)) {
    4.96 +                    for {
    4.97 +                      line <- (0 until visible_lines).iterator
    4.98 +                      start = text_area.getScreenLineStartOffset(line) if start >= 0
    4.99 +                      end = text_area.getScreenLineEndOffset(line) if end >= 0
   4.100 +                      range = Text.Range(start, end)
   4.101 +                      line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
   4.102 +                      if line_cmds.exists(changed.commands)
   4.103 +                    } text_area.invalidateScreenLineRange(line, line)
   4.104                    }
   4.105                  }
   4.106                }
   4.107              }
   4.108            }
   4.109 -
   4.110 -        case bad =>
   4.111 -          System.err.println("command_change_actor: ignoring bad message " + bad)
   4.112 -      }
   4.113 +        }
   4.114      }
   4.115 -  }
   4.116  
   4.117  
   4.118    /* activation */
   4.119 @@ -261,16 +253,16 @@
   4.120      text_area.addKeyListener(key_listener)
   4.121      text_area.addCaretListener(caret_listener)
   4.122      text_area.addLeftOfScrollBar(overview)
   4.123 -    session.raw_edits += main_actor
   4.124 -    session.commands_changed += main_actor
   4.125 +    session.raw_edits += main
   4.126 +    session.commands_changed += main
   4.127    }
   4.128  
   4.129    private def deactivate()
   4.130    {
   4.131      val painter = text_area.getPainter
   4.132  
   4.133 -    session.raw_edits -= main_actor
   4.134 -    session.commands_changed -= main_actor
   4.135 +    session.raw_edits -= main
   4.136 +    session.commands_changed -= main
   4.137      text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
   4.138      text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
   4.139      text_area.removeKeyListener(key_listener)
     5.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
     5.3 @@ -9,8 +9,6 @@
     5.4  
     5.5  import isabelle._
     5.6  
     5.7 -import scala.actors.Actor._
     5.8 -
     5.9  import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
    5.10  import scala.swing.event.ButtonClicked
    5.11  
    5.12 @@ -68,23 +66,16 @@
    5.13    })
    5.14  
    5.15  
    5.16 -  /* main actor */
    5.17 +  /* main */
    5.18  
    5.19 -  private val main_actor = actor {
    5.20 -    loop {
    5.21 -      react {
    5.22 -        case _: Session.Global_Options =>
    5.23 -          Swing_Thread.later { handle_resize() }
    5.24 -
    5.25 -        case bad =>
    5.26 -          System.err.println("Find_Dockable: ignoring bad message " + bad)
    5.27 -      }
    5.28 +  private val main =
    5.29 +    Session.Consumer[Session.Global_Options](getClass.getName) {
    5.30 +      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
    5.31      }
    5.32 -  }
    5.33  
    5.34    override def init()
    5.35    {
    5.36 -    PIDE.session.global_options += main_actor
    5.37 +    PIDE.session.global_options += main
    5.38      handle_resize()
    5.39      find_theorems.activate()
    5.40    }
    5.41 @@ -92,7 +83,7 @@
    5.42    override def exit()
    5.43    {
    5.44      find_theorems.deactivate()
    5.45 -    PIDE.session.global_options -= main_actor
    5.46 +    PIDE.session.global_options -= main
    5.47      delay_resize.revoke()
    5.48    }
    5.49  
     6.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
     6.3 @@ -9,8 +9,6 @@
     6.4  
     6.5  import isabelle._
     6.6  
     6.7 -import scala.actors.Actor._
     6.8 -
     6.9  import scala.swing.Button
    6.10  import scala.swing.event.ButtonClicked
    6.11  
    6.12 @@ -97,30 +95,24 @@
    6.13    add(controls.peer, BorderLayout.NORTH)
    6.14  
    6.15  
    6.16 -  /* main actor */
    6.17 +  /* main */
    6.18  
    6.19 -  private val main_actor = actor {
    6.20 -    loop {
    6.21 -      react {
    6.22 -        case _: Session.Global_Options =>
    6.23 -          Swing_Thread.later { handle_resize() }
    6.24 -
    6.25 -        case bad => System.err.println("Info_Dockable: ignoring bad message " + bad)
    6.26 -      }
    6.27 +  private val main =
    6.28 +    Session.Consumer[Session.Global_Options](getClass.getName) {
    6.29 +      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
    6.30      }
    6.31 -  }
    6.32  
    6.33    override def init()
    6.34    {
    6.35      GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
    6.36 -    PIDE.session.global_options += main_actor
    6.37 +    PIDE.session.global_options += main
    6.38      handle_resize()
    6.39    }
    6.40  
    6.41    override def exit()
    6.42    {
    6.43      GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
    6.44 -    PIDE.session.global_options -= main_actor
    6.45 +    PIDE.session.global_options -= main
    6.46      delay_resize.revoke()
    6.47    }
    6.48  }
     7.1 --- a/src/Tools/jEdit/src/monitor_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
     7.2 +++ b/src/Tools/jEdit/src/monitor_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
     7.3 @@ -9,7 +9,6 @@
     7.4  
     7.5  import isabelle._
     7.6  
     7.7 -import scala.actors.Actor._
     7.8  import scala.swing.{TextArea, ScrollPane, Component}
     7.9  
    7.10  import org.jfree.chart.ChartPanel
    7.11 @@ -35,23 +34,18 @@
    7.12    set_content(new ChartPanel(chart))
    7.13  
    7.14  
    7.15 -  /* main actor */
    7.16 +  /* main */
    7.17  
    7.18 -  private val main_actor = actor {
    7.19 -    loop {
    7.20 -      react {
    7.21 -        case Session.Statistics(props) =>
    7.22 -          Swing_Thread.later {
    7.23 -            rev_stats ::= props
    7.24 -            delay_update.invoke()
    7.25 -          }
    7.26 +  private val main =
    7.27 +    Session.Consumer[Session.Statistics](getClass.getName) {
    7.28 +      case stats =>
    7.29 +        Swing_Thread.later {
    7.30 +          rev_stats ::= stats.props
    7.31 +          delay_update.invoke()
    7.32 +        }
    7.33 +    }
    7.34  
    7.35 -        case bad => System.err.println("Monitor_Dockable: ignoring bad message " + bad)
    7.36 -      }
    7.37 -    }
    7.38 -  }
    7.39 -
    7.40 -  override def init() { PIDE.session.statistics += main_actor }
    7.41 -  override def exit() { PIDE.session.statistics -= main_actor }
    7.42 +  override def init() { PIDE.session.statistics += main }
    7.43 +  override def exit() { PIDE.session.statistics -= main }
    7.44  }
    7.45  
     8.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
     8.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
     8.3 @@ -9,8 +9,6 @@
     8.4  
     8.5  import isabelle._
     8.6  
     8.7 -import scala.actors.Actor._
     8.8 -
     8.9  import scala.swing.{Button, CheckBox}
    8.10  import scala.swing.event.ButtonClicked
    8.11  
    8.12 @@ -82,39 +80,34 @@
    8.13    }
    8.14  
    8.15  
    8.16 -  /* main actor */
    8.17 +  /* main */
    8.18  
    8.19 -  private val main_actor = actor {
    8.20 -    loop {
    8.21 -      react {
    8.22 -        case _: Session.Global_Options =>
    8.23 -          Swing_Thread.later { handle_resize() }
    8.24 +  private val main =
    8.25 +    Session.Consumer[Any](getClass.getName) {
    8.26 +      case _: Session.Global_Options =>
    8.27 +        Swing_Thread.later { handle_resize() }
    8.28  
    8.29 -        case changed: Session.Commands_Changed =>
    8.30 -          val restriction = if (changed.assignment) None else Some(changed.commands)
    8.31 -          Swing_Thread.later { handle_update(do_update, restriction) }
    8.32 +      case changed: Session.Commands_Changed =>
    8.33 +        val restriction = if (changed.assignment) None else Some(changed.commands)
    8.34 +        Swing_Thread.later { handle_update(do_update, restriction) }
    8.35  
    8.36 -        case Session.Caret_Focus =>
    8.37 -          Swing_Thread.later { handle_update(do_update, None) }
    8.38 -
    8.39 -        case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
    8.40 -      }
    8.41 +      case Session.Caret_Focus =>
    8.42 +        Swing_Thread.later { handle_update(do_update, None) }
    8.43      }
    8.44 -  }
    8.45  
    8.46    override def init()
    8.47    {
    8.48 -    PIDE.session.global_options += main_actor
    8.49 -    PIDE.session.commands_changed += main_actor
    8.50 -    PIDE.session.caret_focus += main_actor
    8.51 +    PIDE.session.global_options += main
    8.52 +    PIDE.session.commands_changed += main
    8.53 +    PIDE.session.caret_focus += main
    8.54      handle_update(true, None)
    8.55    }
    8.56  
    8.57    override def exit()
    8.58    {
    8.59 -    PIDE.session.global_options -= main_actor
    8.60 -    PIDE.session.commands_changed -= main_actor
    8.61 -    PIDE.session.caret_focus -= main_actor
    8.62 +    PIDE.session.global_options -= main
    8.63 +    PIDE.session.commands_changed -= main
    8.64 +    PIDE.session.caret_focus -= main
    8.65      delay_resize.revoke()
    8.66    }
    8.67  
     9.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Apr 25 12:27:18 2014 +0200
     9.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Apr 25 12:51:08 2014 +0200
     9.3 @@ -22,8 +22,6 @@
     9.4  
     9.5  import org.gjt.sp.util.SyntaxUtilities
     9.6  
     9.7 -import scala.actors.Actor._
     9.8 -
     9.9  
    9.10  object PIDE
    9.11  {
    9.12 @@ -174,7 +172,7 @@
    9.13  
    9.14    def options_changed()
    9.15    {
    9.16 -    PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
    9.17 +    PIDE.session.global_options.post(Session.Global_Options(PIDE.options.value))
    9.18      Swing_Thread.later { delay_load.invoke() }
    9.19    }
    9.20  
    9.21 @@ -244,34 +242,27 @@
    9.22      }
    9.23  
    9.24  
    9.25 -  /* session manager */
    9.26 +  /* session phase */
    9.27  
    9.28 -  private val session_manager = actor {
    9.29 -    loop {
    9.30 -      react {
    9.31 -        case phase: Session.Phase =>
    9.32 -          phase match {
    9.33 -            case Session.Inactive | Session.Failed =>
    9.34 -              Swing_Thread.later {
    9.35 -                GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
    9.36 -                    "Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog()))
    9.37 -              }
    9.38 +  private val session_phase =
    9.39 +    Session.Consumer[Session.Phase](getClass.getName) {
    9.40 +      case Session.Inactive | Session.Failed =>
    9.41 +        Swing_Thread.later {
    9.42 +          GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
    9.43 +              "Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog()))
    9.44 +        }
    9.45  
    9.46 -            case Session.Ready =>
    9.47 -              PIDE.session.update_options(PIDE.options.value)
    9.48 -              PIDE.init_models()
    9.49 -              Swing_Thread.later { delay_load.invoke() }
    9.50 +      case Session.Ready =>
    9.51 +        PIDE.session.update_options(PIDE.options.value)
    9.52 +        PIDE.init_models()
    9.53 +        Swing_Thread.later { delay_load.invoke() }
    9.54  
    9.55 -            case Session.Shutdown =>
    9.56 -              PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
    9.57 -              Swing_Thread.later { delay_load.revoke() }
    9.58 +      case Session.Shutdown =>
    9.59 +        PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
    9.60 +        Swing_Thread.later { delay_load.revoke() }
    9.61  
    9.62 -            case _ =>
    9.63 -          }
    9.64 -        case bad => System.err.println("session_manager: ignoring bad message " + bad)
    9.65 -      }
    9.66 +      case _ =>
    9.67      }
    9.68 -  }
    9.69  
    9.70  
    9.71    /* main plugin plumbing */
    9.72 @@ -366,7 +357,7 @@
    9.73          override def reparse_limit = PIDE.options.int("editor_reparse_limit")
    9.74        }
    9.75  
    9.76 -      PIDE.session.phase_changed += session_manager
    9.77 +      PIDE.session.phase_changed += session_phase
    9.78        PIDE.startup_failure = None
    9.79      }
    9.80      catch {
    9.81 @@ -385,7 +376,7 @@
    9.82        PIDE.completion_history.value.save()
    9.83      }
    9.84  
    9.85 -    PIDE.session.phase_changed -= session_manager
    9.86 +    PIDE.session.phase_changed -= session_phase
    9.87      PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
    9.88      PIDE.session.stop()
    9.89    }
    10.1 --- a/src/Tools/jEdit/src/protocol_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
    10.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
    10.3 @@ -9,7 +9,6 @@
    10.4  
    10.5  import isabelle._
    10.6  
    10.7 -import scala.actors.Actor._
    10.8  import scala.swing.{TextArea, ScrollPane}
    10.9  
   10.10  import org.gjt.sp.jedit.View
   10.11 @@ -21,22 +20,17 @@
   10.12    set_content(new ScrollPane(text_area))
   10.13  
   10.14  
   10.15 -  /* main actor */
   10.16 +  /* main */
   10.17  
   10.18 -  private val main_actor = actor {
   10.19 -    loop {
   10.20 -      react {
   10.21 -        case input: Prover.Input =>
   10.22 -          Swing_Thread.later { text_area.append(input.toString + "\n\n") }
   10.23 +  private val main =
   10.24 +    Session.Consumer[Prover.Message](getClass.getName) {
   10.25 +      case input: Prover.Input =>
   10.26 +        Swing_Thread.later { text_area.append(input.toString + "\n\n") }
   10.27  
   10.28 -        case output: Prover.Output =>
   10.29 -          Swing_Thread.later { text_area.append(output.message.toString + "\n\n") }
   10.30 -
   10.31 -        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
   10.32 -      }
   10.33 +      case output: Prover.Output =>
   10.34 +        Swing_Thread.later { text_area.append(output.message.toString + "\n\n") }
   10.35      }
   10.36 -  }
   10.37  
   10.38 -  override def init() { PIDE.session.all_messages += main_actor }
   10.39 -  override def exit() { PIDE.session.all_messages -= main_actor }
   10.40 +  override def init() { PIDE.session.all_messages += main }
   10.41 +  override def exit() { PIDE.session.all_messages -= main }
   10.42  }
    11.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
    11.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
    11.3 @@ -9,7 +9,6 @@
    11.4  
    11.5  import isabelle._
    11.6  
    11.7 -import scala.actors.Actor._
    11.8  import scala.swing.{TextArea, ScrollPane}
    11.9  
   11.10  import org.gjt.sp.jedit.View
   11.11 @@ -21,22 +20,17 @@
   11.12    set_content(new ScrollPane(text_area))
   11.13  
   11.14  
   11.15 -  /* main actor */
   11.16 +  /* main */
   11.17  
   11.18 -  private val main_actor = actor {
   11.19 -    loop {
   11.20 -      react {
   11.21 -        case output: Prover.Output =>
   11.22 -          Swing_Thread.later {
   11.23 -            text_area.append(XML.content(output.message))
   11.24 -            if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
   11.25 -          }
   11.26 +  private val main =
   11.27 +    Session.Consumer[Prover.Output](getClass.getName) {
   11.28 +      case output: Prover.Output =>
   11.29 +        Swing_Thread.later {
   11.30 +          text_area.append(XML.content(output.message))
   11.31 +          if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
   11.32 +        }
   11.33 +    }
   11.34  
   11.35 -        case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
   11.36 -      }
   11.37 -    }
   11.38 -  }
   11.39 -
   11.40 -  override def init() { PIDE.session.raw_output_messages += main_actor }
   11.41 -  override def exit() { PIDE.session.raw_output_messages -= main_actor }
   11.42 +  override def init() { PIDE.session.raw_output_messages += main }
   11.43 +  override def exit() { PIDE.session.raw_output_messages -= main }
   11.44  }
    12.1 --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
    12.2 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
    12.3 @@ -9,7 +9,6 @@
    12.4  
    12.5  import isabelle._
    12.6  
    12.7 -import scala.actors.Actor._
    12.8  import scala.swing.{Button, CheckBox, Orientation, Separator}
    12.9  import scala.swing.event.ButtonClicked
   12.10  
   12.11 @@ -127,32 +126,31 @@
   12.12    }
   12.13  
   12.14  
   12.15 -  /* main actor */
   12.16 +  /* main */
   12.17 +
   12.18 +  private val main =
   12.19 +    Session.Consumer[Any](getClass.getName) {
   12.20 +      case _: Session.Global_Options =>
   12.21 +        Swing_Thread.later { handle_resize() }
   12.22  
   12.23 -  private val main_actor = actor {
   12.24 -    loop {
   12.25 -      react {
   12.26 -        case _: Session.Global_Options =>
   12.27 -          Swing_Thread.later { handle_resize() }
   12.28 -        case changed: Session.Commands_Changed =>
   12.29 -          Swing_Thread.later { handle_update(do_update) }
   12.30 -        case Session.Caret_Focus =>
   12.31 -          Swing_Thread.later { handle_update(do_update) }
   12.32 -        case Simplifier_Trace.Event =>
   12.33 -          Swing_Thread.later { handle_update(do_update) }
   12.34 -        case bad => System.err.println("Simplifier_Trace_Dockable: ignoring bad message " + bad)
   12.35 -      }
   12.36 +      case changed: Session.Commands_Changed =>
   12.37 +        Swing_Thread.later { handle_update(do_update) }
   12.38 +
   12.39 +      case Session.Caret_Focus =>
   12.40 +        Swing_Thread.later { handle_update(do_update) }
   12.41 +
   12.42 +      case Simplifier_Trace.Event =>
   12.43 +        Swing_Thread.later { handle_update(do_update) }
   12.44      }
   12.45 -  }
   12.46  
   12.47    override def init()
   12.48    {
   12.49      Swing_Thread.require {}
   12.50  
   12.51 -    PIDE.session.global_options += main_actor
   12.52 -    PIDE.session.commands_changed += main_actor
   12.53 -    PIDE.session.caret_focus += main_actor
   12.54 -    PIDE.session.trace_events += main_actor
   12.55 +    PIDE.session.global_options += main
   12.56 +    PIDE.session.commands_changed += main
   12.57 +    PIDE.session.caret_focus += main
   12.58 +    PIDE.session.trace_events += main
   12.59      handle_update(true)
   12.60    }
   12.61  
   12.62 @@ -160,10 +158,10 @@
   12.63    {
   12.64      Swing_Thread.require {}
   12.65  
   12.66 -    PIDE.session.global_options -= main_actor
   12.67 -    PIDE.session.commands_changed -= main_actor
   12.68 -    PIDE.session.caret_focus -= main_actor
   12.69 -    PIDE.session.trace_events -= main_actor
   12.70 +    PIDE.session.global_options -= main
   12.71 +    PIDE.session.commands_changed -= main
   12.72 +    PIDE.session.caret_focus -= main
   12.73 +    PIDE.session.trace_events -= main
   12.74      delay_resize.revoke()
   12.75    }
   12.76  
    13.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
    13.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
    13.3 @@ -9,8 +9,6 @@
    13.4  
    13.5  import isabelle._
    13.6  
    13.7 -import scala.actors.Actor._
    13.8 -
    13.9  import scala.swing.{Button, Component, Label, TextField, CheckBox}
   13.10  import scala.swing.event.ButtonClicked
   13.11  
   13.12 @@ -135,23 +133,16 @@
   13.13    override def focusOnDefaultComponent { provers.requestFocus }
   13.14  
   13.15  
   13.16 -  /* main actor */
   13.17 +  /* main */
   13.18  
   13.19 -  private val main_actor = actor {
   13.20 -    loop {
   13.21 -      react {
   13.22 -        case _: Session.Global_Options =>
   13.23 -          Swing_Thread.later { update_provers(); handle_resize() }
   13.24 -
   13.25 -        case bad =>
   13.26 -          System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
   13.27 -      }
   13.28 +  private val main =
   13.29 +    Session.Consumer[Session.Global_Options](getClass.getName) {
   13.30 +      case _: Session.Global_Options => Swing_Thread.later { update_provers(); handle_resize() }
   13.31      }
   13.32 -  }
   13.33  
   13.34    override def init()
   13.35    {
   13.36 -    PIDE.session.global_options += main_actor
   13.37 +    PIDE.session.global_options += main
   13.38      update_provers()
   13.39      handle_resize()
   13.40      sledgehammer.activate()
   13.41 @@ -160,7 +151,7 @@
   13.42    override def exit()
   13.43    {
   13.44      sledgehammer.deactivate()
   13.45 -    PIDE.session.global_options -= main_actor
   13.46 +    PIDE.session.global_options -= main
   13.47      delay_resize.revoke()
   13.48    }
   13.49  }
    14.1 --- a/src/Tools/jEdit/src/syslog_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
    14.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
    14.3 @@ -9,7 +9,6 @@
    14.4  
    14.5  import isabelle._
    14.6  
    14.7 -import scala.actors.Actor._
    14.8  import scala.swing.TextArea
    14.9  
   14.10  import org.gjt.sp.jedit.View
   14.11 @@ -32,27 +31,22 @@
   14.12    set_content(syslog)
   14.13  
   14.14  
   14.15 -  /* main actor */
   14.16 +  /* main */
   14.17  
   14.18 -  private val main_actor = actor {
   14.19 -    loop {
   14.20 -      react {
   14.21 -        case output: Prover.Output =>
   14.22 -          if (output.is_syslog) Swing_Thread.later { update_syslog() }
   14.23 -
   14.24 -        case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
   14.25 -      }
   14.26 +  private val main =
   14.27 +    Session.Consumer[Prover.Output](getClass.getName) {
   14.28 +      case output =>
   14.29 +        if (output.is_syslog) Swing_Thread.later { update_syslog() }
   14.30      }
   14.31 -  }
   14.32  
   14.33    override def init()
   14.34    {
   14.35 -    PIDE.session.syslog_messages += main_actor
   14.36 +    PIDE.session.syslog_messages += main
   14.37      update_syslog()
   14.38    }
   14.39  
   14.40    override def exit()
   14.41    {
   14.42 -    PIDE.session.syslog_messages -= main_actor
   14.43 +    PIDE.session.syslog_messages -= main
   14.44    }
   14.45  }
    15.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
    15.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
    15.3 @@ -9,7 +9,6 @@
    15.4  
    15.5  import isabelle._
    15.6  
    15.7 -import scala.actors.Actor._
    15.8  import scala.swing.{Button, TextArea, Label, ListView, Alignment,
    15.9    ScrollPane, Component, CheckBox, BorderPanel}
   15.10  import scala.swing.event.{MouseClicked, MouseMoved}
   15.11 @@ -216,35 +215,30 @@
   15.12    }
   15.13  
   15.14  
   15.15 -  /* main actor */
   15.16 +  /* main */
   15.17  
   15.18 -  private val main_actor = actor {
   15.19 -    loop {
   15.20 -      react {
   15.21 -        case phase: Session.Phase =>
   15.22 -          Swing_Thread.later { handle_phase(phase) }
   15.23 +  private val main =
   15.24 +    Session.Consumer[Any](getClass.getName) {
   15.25 +      case phase: Session.Phase =>
   15.26 +        Swing_Thread.later { handle_phase(phase) }
   15.27  
   15.28 -        case _: Session.Global_Options =>
   15.29 -          Swing_Thread.later {
   15.30 -            continuous_checking.load()
   15.31 -            logic.load ()
   15.32 -            update_nodes_required()
   15.33 -            status.repaint()
   15.34 -          }
   15.35 +      case _: Session.Global_Options =>
   15.36 +        Swing_Thread.later {
   15.37 +          continuous_checking.load()
   15.38 +          logic.load ()
   15.39 +          update_nodes_required()
   15.40 +          status.repaint()
   15.41 +        }
   15.42  
   15.43 -        case changed: Session.Commands_Changed =>
   15.44 -          Swing_Thread.later { handle_update(Some(changed.nodes)) }
   15.45 -
   15.46 -        case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad)
   15.47 -      }
   15.48 +      case changed: Session.Commands_Changed =>
   15.49 +        Swing_Thread.later { handle_update(Some(changed.nodes)) }
   15.50      }
   15.51 -  }
   15.52  
   15.53    override def init()
   15.54    {
   15.55 -    PIDE.session.phase_changed += main_actor
   15.56 -    PIDE.session.global_options += main_actor
   15.57 -    PIDE.session.commands_changed += main_actor
   15.58 +    PIDE.session.phase_changed += main
   15.59 +    PIDE.session.global_options += main
   15.60 +    PIDE.session.commands_changed += main
   15.61  
   15.62      handle_phase(PIDE.session.phase)
   15.63      handle_update()
   15.64 @@ -252,8 +246,8 @@
   15.65  
   15.66    override def exit()
   15.67    {
   15.68 -    PIDE.session.phase_changed -= main_actor
   15.69 -    PIDE.session.global_options -= main_actor
   15.70 -    PIDE.session.commands_changed -= main_actor
   15.71 +    PIDE.session.phase_changed -= main
   15.72 +    PIDE.session.global_options -= main
   15.73 +    PIDE.session.commands_changed -= main
   15.74    }
   15.75  }
    16.1 --- a/src/Tools/jEdit/src/timing_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
    16.2 +++ b/src/Tools/jEdit/src/timing_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
    16.3 @@ -9,7 +9,6 @@
    16.4  
    16.5  import isabelle._
    16.6  
    16.7 -import scala.actors.Actor._
    16.8  import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField}
    16.9  import scala.swing.event.{MouseClicked, ValueChanged}
   16.10  
   16.11 @@ -200,27 +199,22 @@
   16.12    }
   16.13  
   16.14  
   16.15 -  /* main actor */
   16.16 +  /* main */
   16.17  
   16.18 -  private val main_actor = actor {
   16.19 -    loop {
   16.20 -      react {
   16.21 -        case changed: Session.Commands_Changed =>
   16.22 -          Swing_Thread.later { handle_update(Some(changed.nodes)) }
   16.23 -
   16.24 -        case bad => System.err.println("Timing_Dockable: ignoring bad message " + bad)
   16.25 -      }
   16.26 +  private val main =
   16.27 +    Session.Consumer[Session.Commands_Changed](getClass.getName) {
   16.28 +      case changed =>
   16.29 +        Swing_Thread.later { handle_update(Some(changed.nodes)) }
   16.30      }
   16.31 -  }
   16.32  
   16.33    override def init()
   16.34    {
   16.35 -    PIDE.session.commands_changed += main_actor
   16.36 +    PIDE.session.commands_changed += main
   16.37      handle_update()
   16.38    }
   16.39  
   16.40    override def exit()
   16.41    {
   16.42 -    PIDE.session.commands_changed -= main_actor
   16.43 +    PIDE.session.commands_changed -= main
   16.44    }
   16.45  }