clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
--- 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)
--- 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*)
--- 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)
--- 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)
--- 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()
}
--- 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()
}
}
--- 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 }
}
--- 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()
}
--- 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()
}
--- 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 }
}
--- 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 }
}
--- 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()
}
--- 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()
}
}
--- 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
}
}
--- 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
}
}
--- 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
}
}