# HG changeset patch
# User wenzelm
# Date 1398423068 -7200
# Node ID 52125652e82a0df818db29335d4c697e8e8b6989
# Parent  061f83259922c093f4eda6f9149b72c5d0e8c819
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;

diff -r 061f83259922 -r 52125652e82a src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -8,9 +8,6 @@
 package isabelle
 
 
-import scala.actors.Actor._
-
-
 object Query_Operation
 {
   object Status extends Enumeration
@@ -33,12 +30,12 @@
 
   /* implicit state -- owned by Swing thread */
 
-  private var current_location: Option[Command] = None
-  private var current_query: List[String] = Nil
-  private var current_update_pending = false
-  private var current_output: List[XML.Tree] = Nil
-  private var current_status = Query_Operation.Status.FINISHED
-  private var current_exec_id = Document_ID.none
+  @volatile private var current_location: Option[Command] = None
+  @volatile private var current_query: List[String] = Nil
+  @volatile private var current_update_pending = false
+  @volatile private var current_output: List[XML.Tree] = Nil
+  @volatile private var current_status = Query_Operation.Status.FINISHED
+  @volatile private var current_exec_id = Document_ID.none
 
   private def reset_state()
   {
@@ -209,32 +206,27 @@
   }
 
 
-  /* main actor */
+  /* main */
 
-  private val main_actor = actor {
-    loop {
-      react {
-        case changed: Session.Commands_Changed =>
-          current_location match {
-            case Some(command)
-            if current_update_pending ||
-              (current_status != Query_Operation.Status.FINISHED &&
-                changed.commands.contains(command)) =>
-              Swing_Thread.later { content_update() }
-            case _ =>
-          }
-        case bad =>
-          System.err.println("Query_Operation: ignoring bad message " + bad)
-      }
+  private val main =
+    Session.Consumer[Session.Commands_Changed](getClass.getName) {
+      case changed =>
+        current_location match {
+          case Some(command)
+          if current_update_pending ||
+            (current_status != Query_Operation.Status.FINISHED &&
+              changed.commands.contains(command)) =>
+            Swing_Thread.later { content_update() }
+          case _ =>
+        }
     }
-  }
 
   def activate() {
-    editor.session.commands_changed += main_actor
+    editor.session.commands_changed += main
   }
 
   def deactivate() {
-    editor.session.commands_changed -= main_actor
+    editor.session.commands_changed -= main
     remove_overlay()
     reset_state()
     consume_output(Document.Snapshot.init, Command.Results.empty, Nil)
diff -r 061f83259922 -r 52125652e82a src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -16,6 +16,36 @@
 
 object Session
 {
+  /* outlets */
+
+  object Consumer
+  {
+    def apply[A](name: String)(consume: A => Unit): Consumer[A] =
+      new Consumer[A](name, consume)
+  }
+  final class Consumer[-A] private(val name: String, val consume: A => Unit)
+
+  class Outlet[A](dispatcher: Consumer_Thread[() => Unit])
+  {
+    private val consumers = Synchronized(List.empty[Consumer[A]])
+
+    def += (c: Consumer[A]) { consumers.change(Library.update(c)) }
+    def -= (c: Consumer[A]) { consumers.change(Library.remove(c)) }
+
+    def post(a: A)
+    {
+      for (c <- consumers.value.iterator) {
+        dispatcher.send(() =>
+          try { c.consume(a) }
+          catch {
+            case exn: Throwable =>
+              System.err.println("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
+          })
+      }
+    }
+  }
+
+
   /* change */
 
   sealed case class Change(
@@ -134,18 +164,21 @@
   def reparse_limit: Int = 0
 
 
-  /* pervasive event buses */
+  /* outlets */
+
+  private val dispatcher =
+    Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true }
 
-  val statistics = new Event_Bus[Session.Statistics]
-  val global_options = new Event_Bus[Session.Global_Options]
-  val caret_focus = new Event_Bus[Session.Caret_Focus.type]
-  val raw_edits = new Event_Bus[Session.Raw_Edits]
-  val commands_changed = new Event_Bus[Session.Commands_Changed]
-  val phase_changed = new Event_Bus[Session.Phase]
-  val syslog_messages = new Event_Bus[Prover.Output]
-  val raw_output_messages = new Event_Bus[Prover.Output]
-  val all_messages = new Event_Bus[Prover.Message]  // potential bottle-neck
-  val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
+  val statistics = new Session.Outlet[Session.Statistics](dispatcher)
+  val global_options = new Session.Outlet[Session.Global_Options](dispatcher)
+  val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher)
+  val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher)
+  val commands_changed = new Session.Outlet[Session.Commands_Changed](dispatcher)
+  val phase_changed = new Session.Outlet[Session.Phase](dispatcher)
+  val syslog_messages = new Session.Outlet[Prover.Output](dispatcher)
+  val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher)
+  val all_messages = new Session.Outlet[Prover.Message](dispatcher)  // potential bottle-neck
+  val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher)
 
 
 
@@ -163,7 +196,7 @@
 
       def flush(): Unit = synchronized {
         if (assignment || !nodes.isEmpty || !commands.isEmpty)
-          commands_changed.event(Session.Commands_Changed(assignment, nodes, commands))
+          commands_changed.post(Session.Commands_Changed(assignment, nodes, commands))
         assignment = false
         nodes = Set.empty
         commands = Set.empty
@@ -223,7 +256,7 @@
   private def phase_=(new_phase: Session.Phase)
   {
     _phase = new_phase
-    phase_changed.event(new_phase)
+    phase_changed.post(new_phase)
   }
   def phase = _phase
   def is_ready: Boolean = phase == Session.Ready
@@ -349,7 +382,7 @@
       val version = Future.promise[Document.Version]
       global_state.change(_.continue_history(previous, edits, version))
 
-      raw_edits.event(Session.Raw_Edits(doc_blobs, edits))
+      raw_edits.post(Session.Raw_Edits(doc_blobs, edits))
       change_parser.send(Text_Edits(previous, doc_blobs, edits, version))
     }
     //}}}
@@ -458,7 +491,7 @@
                 }
 
               case Markup.ML_Statistics(props) =>
-                statistics.event(Session.Statistics(props))
+                statistics.post(Session.Statistics(props))
 
               case Markup.Task_Statistics(props) =>
                 // FIXME
@@ -479,7 +512,7 @@
               if (rc == 0) phase = Session.Inactive
               else phase = Session.Failed
 
-            case _ => raw_output_messages.event(output)
+            case _ => raw_output_messages.post(output)
           }
         }
     }
@@ -512,7 +545,7 @@
               prover.get.options(options)
               handle_raw_edits(Document.Blobs.empty, Nil)
             }
-            global_options.event(Session.Global_Options(options))
+            global_options.post(Session.Global_Options(options))
 
           case Cancel_Exec(exec_id) if prover.isDefined =>
             prover.get.cancel_exec(exec_id)
@@ -530,13 +563,13 @@
           case Messages(msgs) =>
             msgs foreach {
               case input: Prover.Input =>
-                all_messages.event(input)
+                all_messages.post(input)
 
               case output: Prover.Output =>
-                if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
+                if (output.is_stdout || output.is_stderr) raw_output_messages.post(output)
                 else handle_output(output)
-                if (output.is_syslog) syslog_messages.event(output)
-                all_messages.event(output)
+                if (output.is_syslog) syslog_messages.post(output)
+                all_messages.post(output)
             }
 
           case change: Session.Change if prover.isDefined =>
@@ -562,6 +595,7 @@
     change_parser.shutdown()
     change_buffer.shutdown()
     manager.shutdown()
+    dispatcher.shutdown()
   }
 
   def protocol_command(name: String, args: String*)
diff -r 061f83259922 -r 52125652e82a src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -287,7 +287,7 @@
           }
 
           do_reply(session, serial, answer)
-          session.trace_events.event(Event)
+          session.trace_events.post(Event)
 
         case bad =>
           System.err.println("context_manager: bad message " + bad)
diff -r 061f83259922 -r 52125652e82a src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -10,8 +10,6 @@
 
 import isabelle._
 
-import scala.actors.Actor._
-
 import java.awt.Graphics2D
 import java.awt.event.KeyEvent
 import javax.swing.event.{CaretListener, CaretEvent}
@@ -176,7 +174,7 @@
 
   private val delay_caret_update =
     Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
-      session.caret_focus.event(Session.Caret_Focus)
+      session.caret_focus.post(Session.Caret_Focus)
     }
 
   private val caret_listener = new CaretListener {
@@ -193,60 +191,54 @@
   }
 
 
-  /* main actor */
+  /* main */
 
-  private val main_actor = actor {
-    loop {
-      react {
-        case _: Session.Raw_Edits =>
-          Swing_Thread.later {
-            overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
-          }
+  private val main =
+    Session.Consumer[Any](getClass.getName) {
+      case _: Session.Raw_Edits =>
+        Swing_Thread.later {
+          overview.delay_repaint.postpone(PIDE.options.seconds("editor_input_delay"))
+        }
 
-        case changed: Session.Commands_Changed =>
-          val buffer = model.buffer
-          Swing_Thread.later {
-            JEdit_Lib.buffer_lock(buffer) {
-              if (model.buffer == text_area.getBuffer) {
-                val snapshot = model.snapshot()
+      case changed: Session.Commands_Changed =>
+        val buffer = model.buffer
+        Swing_Thread.later {
+          JEdit_Lib.buffer_lock(buffer) {
+            if (model.buffer == text_area.getBuffer) {
+              val snapshot = model.snapshot()
 
-                val load_changed =
-                  snapshot.load_commands.exists(changed.commands.contains)
+              val load_changed =
+                snapshot.load_commands.exists(changed.commands.contains)
 
-                if (changed.assignment || load_changed ||
-                    (changed.nodes.contains(model.node_name) &&
-                     changed.commands.exists(snapshot.node.commands.contains)))
-                  Swing_Thread.later { overview.delay_repaint.invoke() }
+              if (changed.assignment || load_changed ||
+                  (changed.nodes.contains(model.node_name) &&
+                   changed.commands.exists(snapshot.node.commands.contains)))
+                Swing_Thread.later { overview.delay_repaint.invoke() }
 
-                val visible_lines = text_area.getVisibleLines
-                if (visible_lines > 0) {
-                  if (changed.assignment || load_changed)
-                    text_area.invalidateScreenLineRange(0, visible_lines)
-                  else {
-                    val visible_range = JEdit_Lib.visible_range(text_area).get
-                    val visible_iterator =
-                      snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
-                    if (visible_iterator.exists(changed.commands)) {
-                      for {
-                        line <- (0 until visible_lines).iterator
-                        start = text_area.getScreenLineStartOffset(line) if start >= 0
-                        end = text_area.getScreenLineEndOffset(line) if end >= 0
-                        range = Text.Range(start, end)
-                        line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
-                        if line_cmds.exists(changed.commands)
-                      } text_area.invalidateScreenLineRange(line, line)
-                    }
+              val visible_lines = text_area.getVisibleLines
+              if (visible_lines > 0) {
+                if (changed.assignment || load_changed)
+                  text_area.invalidateScreenLineRange(0, visible_lines)
+                else {
+                  val visible_range = JEdit_Lib.visible_range(text_area).get
+                  val visible_iterator =
+                    snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
+                  if (visible_iterator.exists(changed.commands)) {
+                    for {
+                      line <- (0 until visible_lines).iterator
+                      start = text_area.getScreenLineStartOffset(line) if start >= 0
+                      end = text_area.getScreenLineEndOffset(line) if end >= 0
+                      range = Text.Range(start, end)
+                      line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
+                      if line_cmds.exists(changed.commands)
+                    } text_area.invalidateScreenLineRange(line, line)
                   }
                 }
               }
             }
           }
-
-        case bad =>
-          System.err.println("command_change_actor: ignoring bad message " + bad)
-      }
+        }
     }
-  }
 
 
   /* activation */
@@ -261,16 +253,16 @@
     text_area.addKeyListener(key_listener)
     text_area.addCaretListener(caret_listener)
     text_area.addLeftOfScrollBar(overview)
-    session.raw_edits += main_actor
-    session.commands_changed += main_actor
+    session.raw_edits += main
+    session.commands_changed += main
   }
 
   private def deactivate()
   {
     val painter = text_area.getPainter
 
-    session.raw_edits -= main_actor
-    session.commands_changed -= main_actor
+    session.raw_edits -= main
+    session.commands_changed -= main
     text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
     text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
     text_area.removeKeyListener(key_listener)
diff -r 061f83259922 -r 52125652e82a src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -9,8 +9,6 @@
 
 import isabelle._
 
-import scala.actors.Actor._
-
 import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
 import scala.swing.event.ButtonClicked
 
@@ -68,23 +66,16 @@
   })
 
 
-  /* main actor */
+  /* main */
 
-  private val main_actor = actor {
-    loop {
-      react {
-        case _: Session.Global_Options =>
-          Swing_Thread.later { handle_resize() }
-
-        case bad =>
-          System.err.println("Find_Dockable: ignoring bad message " + bad)
-      }
+  private val main =
+    Session.Consumer[Session.Global_Options](getClass.getName) {
+      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
     }
-  }
 
   override def init()
   {
-    PIDE.session.global_options += main_actor
+    PIDE.session.global_options += main
     handle_resize()
     find_theorems.activate()
   }
@@ -92,7 +83,7 @@
   override def exit()
   {
     find_theorems.deactivate()
-    PIDE.session.global_options -= main_actor
+    PIDE.session.global_options -= main
     delay_resize.revoke()
   }
 
diff -r 061f83259922 -r 52125652e82a src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -9,8 +9,6 @@
 
 import isabelle._
 
-import scala.actors.Actor._
-
 import scala.swing.Button
 import scala.swing.event.ButtonClicked
 
@@ -97,30 +95,24 @@
   add(controls.peer, BorderLayout.NORTH)
 
 
-  /* main actor */
+  /* main */
 
-  private val main_actor = actor {
-    loop {
-      react {
-        case _: Session.Global_Options =>
-          Swing_Thread.later { handle_resize() }
-
-        case bad => System.err.println("Info_Dockable: ignoring bad message " + bad)
-      }
+  private val main =
+    Session.Consumer[Session.Global_Options](getClass.getName) {
+      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
     }
-  }
 
   override def init()
   {
     GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
-    PIDE.session.global_options += main_actor
+    PIDE.session.global_options += main
     handle_resize()
   }
 
   override def exit()
   {
     GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
-    PIDE.session.global_options -= main_actor
+    PIDE.session.global_options -= main
     delay_resize.revoke()
   }
 }
diff -r 061f83259922 -r 52125652e82a src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -9,7 +9,6 @@
 
 import isabelle._
 
-import scala.actors.Actor._
 import scala.swing.{TextArea, ScrollPane, Component}
 
 import org.jfree.chart.ChartPanel
@@ -35,23 +34,18 @@
   set_content(new ChartPanel(chart))
 
 
-  /* main actor */
+  /* main */
 
-  private val main_actor = actor {
-    loop {
-      react {
-        case Session.Statistics(props) =>
-          Swing_Thread.later {
-            rev_stats ::= props
-            delay_update.invoke()
-          }
+  private val main =
+    Session.Consumer[Session.Statistics](getClass.getName) {
+      case stats =>
+        Swing_Thread.later {
+          rev_stats ::= stats.props
+          delay_update.invoke()
+        }
+    }
 
-        case bad => System.err.println("Monitor_Dockable: ignoring bad message " + bad)
-      }
-    }
-  }
-
-  override def init() { PIDE.session.statistics += main_actor }
-  override def exit() { PIDE.session.statistics -= main_actor }
+  override def init() { PIDE.session.statistics += main }
+  override def exit() { PIDE.session.statistics -= main }
 }
 
diff -r 061f83259922 -r 52125652e82a src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -9,8 +9,6 @@
 
 import isabelle._
 
-import scala.actors.Actor._
-
 import scala.swing.{Button, CheckBox}
 import scala.swing.event.ButtonClicked
 
@@ -82,39 +80,34 @@
   }
 
 
-  /* main actor */
+  /* main */
 
-  private val main_actor = actor {
-    loop {
-      react {
-        case _: Session.Global_Options =>
-          Swing_Thread.later { handle_resize() }
+  private val main =
+    Session.Consumer[Any](getClass.getName) {
+      case _: Session.Global_Options =>
+        Swing_Thread.later { handle_resize() }
 
-        case changed: Session.Commands_Changed =>
-          val restriction = if (changed.assignment) None else Some(changed.commands)
-          Swing_Thread.later { handle_update(do_update, restriction) }
+      case changed: Session.Commands_Changed =>
+        val restriction = if (changed.assignment) None else Some(changed.commands)
+        Swing_Thread.later { handle_update(do_update, restriction) }
 
-        case Session.Caret_Focus =>
-          Swing_Thread.later { handle_update(do_update, None) }
-
-        case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
-      }
+      case Session.Caret_Focus =>
+        Swing_Thread.later { handle_update(do_update, None) }
     }
-  }
 
   override def init()
   {
-    PIDE.session.global_options += main_actor
-    PIDE.session.commands_changed += main_actor
-    PIDE.session.caret_focus += main_actor
+    PIDE.session.global_options += main
+    PIDE.session.commands_changed += main
+    PIDE.session.caret_focus += main
     handle_update(true, None)
   }
 
   override def exit()
   {
-    PIDE.session.global_options -= main_actor
-    PIDE.session.commands_changed -= main_actor
-    PIDE.session.caret_focus -= main_actor
+    PIDE.session.global_options -= main
+    PIDE.session.commands_changed -= main
+    PIDE.session.caret_focus -= main
     delay_resize.revoke()
   }
 
diff -r 061f83259922 -r 52125652e82a src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -22,8 +22,6 @@
 
 import org.gjt.sp.util.SyntaxUtilities
 
-import scala.actors.Actor._
-
 
 object PIDE
 {
@@ -174,7 +172,7 @@
 
   def options_changed()
   {
-    PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
+    PIDE.session.global_options.post(Session.Global_Options(PIDE.options.value))
     Swing_Thread.later { delay_load.invoke() }
   }
 
@@ -244,34 +242,27 @@
     }
 
 
-  /* session manager */
+  /* session phase */
 
-  private val session_manager = actor {
-    loop {
-      react {
-        case phase: Session.Phase =>
-          phase match {
-            case Session.Inactive | Session.Failed =>
-              Swing_Thread.later {
-                GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
-                    "Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog()))
-              }
+  private val session_phase =
+    Session.Consumer[Session.Phase](getClass.getName) {
+      case Session.Inactive | Session.Failed =>
+        Swing_Thread.later {
+          GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
+              "Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog()))
+        }
 
-            case Session.Ready =>
-              PIDE.session.update_options(PIDE.options.value)
-              PIDE.init_models()
-              Swing_Thread.later { delay_load.invoke() }
+      case Session.Ready =>
+        PIDE.session.update_options(PIDE.options.value)
+        PIDE.init_models()
+        Swing_Thread.later { delay_load.invoke() }
 
-            case Session.Shutdown =>
-              PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
-              Swing_Thread.later { delay_load.revoke() }
+      case Session.Shutdown =>
+        PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
+        Swing_Thread.later { delay_load.revoke() }
 
-            case _ =>
-          }
-        case bad => System.err.println("session_manager: ignoring bad message " + bad)
-      }
+      case _ =>
     }
-  }
 
 
   /* main plugin plumbing */
@@ -366,7 +357,7 @@
         override def reparse_limit = PIDE.options.int("editor_reparse_limit")
       }
 
-      PIDE.session.phase_changed += session_manager
+      PIDE.session.phase_changed += session_phase
       PIDE.startup_failure = None
     }
     catch {
@@ -385,7 +376,7 @@
       PIDE.completion_history.value.save()
     }
 
-    PIDE.session.phase_changed -= session_manager
+    PIDE.session.phase_changed -= session_phase
     PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
     PIDE.session.stop()
   }
diff -r 061f83259922 -r 52125652e82a src/Tools/jEdit/src/protocol_dockable.scala
--- a/src/Tools/jEdit/src/protocol_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Tools/jEdit/src/protocol_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -9,7 +9,6 @@
 
 import isabelle._
 
-import scala.actors.Actor._
 import scala.swing.{TextArea, ScrollPane}
 
 import org.gjt.sp.jedit.View
@@ -21,22 +20,17 @@
   set_content(new ScrollPane(text_area))
 
 
-  /* main actor */
+  /* main */
 
-  private val main_actor = actor {
-    loop {
-      react {
-        case input: Prover.Input =>
-          Swing_Thread.later { text_area.append(input.toString + "\n\n") }
+  private val main =
+    Session.Consumer[Prover.Message](getClass.getName) {
+      case input: Prover.Input =>
+        Swing_Thread.later { text_area.append(input.toString + "\n\n") }
 
-        case output: Prover.Output =>
-          Swing_Thread.later { text_area.append(output.message.toString + "\n\n") }
-
-        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
-      }
+      case output: Prover.Output =>
+        Swing_Thread.later { text_area.append(output.message.toString + "\n\n") }
     }
-  }
 
-  override def init() { PIDE.session.all_messages += main_actor }
-  override def exit() { PIDE.session.all_messages -= main_actor }
+  override def init() { PIDE.session.all_messages += main }
+  override def exit() { PIDE.session.all_messages -= main }
 }
diff -r 061f83259922 -r 52125652e82a src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -9,7 +9,6 @@
 
 import isabelle._
 
-import scala.actors.Actor._
 import scala.swing.{TextArea, ScrollPane}
 
 import org.gjt.sp.jedit.View
@@ -21,22 +20,17 @@
   set_content(new ScrollPane(text_area))
 
 
-  /* main actor */
+  /* main */
 
-  private val main_actor = actor {
-    loop {
-      react {
-        case output: Prover.Output =>
-          Swing_Thread.later {
-            text_area.append(XML.content(output.message))
-            if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
-          }
+  private val main =
+    Session.Consumer[Prover.Output](getClass.getName) {
+      case output: Prover.Output =>
+        Swing_Thread.later {
+          text_area.append(XML.content(output.message))
+          if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
+        }
+    }
 
-        case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
-      }
-    }
-  }
-
-  override def init() { PIDE.session.raw_output_messages += main_actor }
-  override def exit() { PIDE.session.raw_output_messages -= main_actor }
+  override def init() { PIDE.session.raw_output_messages += main }
+  override def exit() { PIDE.session.raw_output_messages -= main }
 }
diff -r 061f83259922 -r 52125652e82a src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -9,7 +9,6 @@
 
 import isabelle._
 
-import scala.actors.Actor._
 import scala.swing.{Button, CheckBox, Orientation, Separator}
 import scala.swing.event.ButtonClicked
 
@@ -127,32 +126,31 @@
   }
 
 
-  /* main actor */
+  /* main */
+
+  private val main =
+    Session.Consumer[Any](getClass.getName) {
+      case _: Session.Global_Options =>
+        Swing_Thread.later { handle_resize() }
 
-  private val main_actor = actor {
-    loop {
-      react {
-        case _: Session.Global_Options =>
-          Swing_Thread.later { handle_resize() }
-        case changed: Session.Commands_Changed =>
-          Swing_Thread.later { handle_update(do_update) }
-        case Session.Caret_Focus =>
-          Swing_Thread.later { handle_update(do_update) }
-        case Simplifier_Trace.Event =>
-          Swing_Thread.later { handle_update(do_update) }
-        case bad => System.err.println("Simplifier_Trace_Dockable: ignoring bad message " + bad)
-      }
+      case changed: Session.Commands_Changed =>
+        Swing_Thread.later { handle_update(do_update) }
+
+      case Session.Caret_Focus =>
+        Swing_Thread.later { handle_update(do_update) }
+
+      case Simplifier_Trace.Event =>
+        Swing_Thread.later { handle_update(do_update) }
     }
-  }
 
   override def init()
   {
     Swing_Thread.require {}
 
-    PIDE.session.global_options += main_actor
-    PIDE.session.commands_changed += main_actor
-    PIDE.session.caret_focus += main_actor
-    PIDE.session.trace_events += main_actor
+    PIDE.session.global_options += main
+    PIDE.session.commands_changed += main
+    PIDE.session.caret_focus += main
+    PIDE.session.trace_events += main
     handle_update(true)
   }
 
@@ -160,10 +158,10 @@
   {
     Swing_Thread.require {}
 
-    PIDE.session.global_options -= main_actor
-    PIDE.session.commands_changed -= main_actor
-    PIDE.session.caret_focus -= main_actor
-    PIDE.session.trace_events -= main_actor
+    PIDE.session.global_options -= main
+    PIDE.session.commands_changed -= main
+    PIDE.session.caret_focus -= main
+    PIDE.session.trace_events -= main
     delay_resize.revoke()
   }
 
diff -r 061f83259922 -r 52125652e82a src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -9,8 +9,6 @@
 
 import isabelle._
 
-import scala.actors.Actor._
-
 import scala.swing.{Button, Component, Label, TextField, CheckBox}
 import scala.swing.event.ButtonClicked
 
@@ -135,23 +133,16 @@
   override def focusOnDefaultComponent { provers.requestFocus }
 
 
-  /* main actor */
+  /* main */
 
-  private val main_actor = actor {
-    loop {
-      react {
-        case _: Session.Global_Options =>
-          Swing_Thread.later { update_provers(); handle_resize() }
-
-        case bad =>
-          System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
-      }
+  private val main =
+    Session.Consumer[Session.Global_Options](getClass.getName) {
+      case _: Session.Global_Options => Swing_Thread.later { update_provers(); handle_resize() }
     }
-  }
 
   override def init()
   {
-    PIDE.session.global_options += main_actor
+    PIDE.session.global_options += main
     update_provers()
     handle_resize()
     sledgehammer.activate()
@@ -160,7 +151,7 @@
   override def exit()
   {
     sledgehammer.deactivate()
-    PIDE.session.global_options -= main_actor
+    PIDE.session.global_options -= main
     delay_resize.revoke()
   }
 }
diff -r 061f83259922 -r 52125652e82a src/Tools/jEdit/src/syslog_dockable.scala
--- a/src/Tools/jEdit/src/syslog_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -9,7 +9,6 @@
 
 import isabelle._
 
-import scala.actors.Actor._
 import scala.swing.TextArea
 
 import org.gjt.sp.jedit.View
@@ -32,27 +31,22 @@
   set_content(syslog)
 
 
-  /* main actor */
+  /* main */
 
-  private val main_actor = actor {
-    loop {
-      react {
-        case output: Prover.Output =>
-          if (output.is_syslog) Swing_Thread.later { update_syslog() }
-
-        case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
-      }
+  private val main =
+    Session.Consumer[Prover.Output](getClass.getName) {
+      case output =>
+        if (output.is_syslog) Swing_Thread.later { update_syslog() }
     }
-  }
 
   override def init()
   {
-    PIDE.session.syslog_messages += main_actor
+    PIDE.session.syslog_messages += main
     update_syslog()
   }
 
   override def exit()
   {
-    PIDE.session.syslog_messages -= main_actor
+    PIDE.session.syslog_messages -= main
   }
 }
diff -r 061f83259922 -r 52125652e82a src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -9,7 +9,6 @@
 
 import isabelle._
 
-import scala.actors.Actor._
 import scala.swing.{Button, TextArea, Label, ListView, Alignment,
   ScrollPane, Component, CheckBox, BorderPanel}
 import scala.swing.event.{MouseClicked, MouseMoved}
@@ -216,35 +215,30 @@
   }
 
 
-  /* main actor */
+  /* main */
 
-  private val main_actor = actor {
-    loop {
-      react {
-        case phase: Session.Phase =>
-          Swing_Thread.later { handle_phase(phase) }
+  private val main =
+    Session.Consumer[Any](getClass.getName) {
+      case phase: Session.Phase =>
+        Swing_Thread.later { handle_phase(phase) }
 
-        case _: Session.Global_Options =>
-          Swing_Thread.later {
-            continuous_checking.load()
-            logic.load ()
-            update_nodes_required()
-            status.repaint()
-          }
+      case _: Session.Global_Options =>
+        Swing_Thread.later {
+          continuous_checking.load()
+          logic.load ()
+          update_nodes_required()
+          status.repaint()
+        }
 
-        case changed: Session.Commands_Changed =>
-          Swing_Thread.later { handle_update(Some(changed.nodes)) }
-
-        case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad)
-      }
+      case changed: Session.Commands_Changed =>
+        Swing_Thread.later { handle_update(Some(changed.nodes)) }
     }
-  }
 
   override def init()
   {
-    PIDE.session.phase_changed += main_actor
-    PIDE.session.global_options += main_actor
-    PIDE.session.commands_changed += main_actor
+    PIDE.session.phase_changed += main
+    PIDE.session.global_options += main
+    PIDE.session.commands_changed += main
 
     handle_phase(PIDE.session.phase)
     handle_update()
@@ -252,8 +246,8 @@
 
   override def exit()
   {
-    PIDE.session.phase_changed -= main_actor
-    PIDE.session.global_options -= main_actor
-    PIDE.session.commands_changed -= main_actor
+    PIDE.session.phase_changed -= main
+    PIDE.session.global_options -= main
+    PIDE.session.commands_changed -= main
   }
 }
diff -r 061f83259922 -r 52125652e82a src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
@@ -9,7 +9,6 @@
 
 import isabelle._
 
-import scala.actors.Actor._
 import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField}
 import scala.swing.event.{MouseClicked, ValueChanged}
 
@@ -200,27 +199,22 @@
   }
 
 
-  /* main actor */
+  /* main */
 
-  private val main_actor = actor {
-    loop {
-      react {
-        case changed: Session.Commands_Changed =>
-          Swing_Thread.later { handle_update(Some(changed.nodes)) }
-
-        case bad => System.err.println("Timing_Dockable: ignoring bad message " + bad)
-      }
+  private val main =
+    Session.Consumer[Session.Commands_Changed](getClass.getName) {
+      case changed =>
+        Swing_Thread.later { handle_update(Some(changed.nodes)) }
     }
-  }
 
   override def init()
   {
-    PIDE.session.commands_changed += main_actor
+    PIDE.session.commands_changed += main
     handle_update()
   }
 
   override def exit()
   {
-    PIDE.session.commands_changed -= main_actor
+    PIDE.session.commands_changed -= main
   }
 }