Command.toString: include id for debugging;
Command.consume: explicit forward, avoid dependency on Session and side-effect on event bus;
State.+ without side-effect on event bus;
Session.commands_changed: delayed command changes (outside of Swing thread), also subsumes former Session.results;
Document_View: tuned commands_changed handling and caret listening;
Document_View.selected_command: proper function, not event handler state;
Output_Dockable: directly act upon commands_changed, not caret events (via former Session.results);
--- a/src/Pure/PIDE/command.scala Wed May 26 18:19:36 2010 +0200
+++ b/src/Pure/PIDE/command.scala Thu May 27 00:47:15 2010 +0200
@@ -13,6 +13,9 @@
import scala.collection.mutable
+case class Command_Set(set: Set[Command])
+
+
object Command
{
object Status extends Enumeration
@@ -29,10 +32,10 @@
command_id: Option[String], offset: Option[Int])
}
-
class Command(
val id: Isar_Document.Command_ID,
- val span: Thy_Syntax.Span)
+ val span: Thy_Syntax.Span,
+ val static_parent: Option[Command] = None)
extends Session.Entity
{
/* classification */
@@ -42,7 +45,9 @@
def is_malformed: Boolean = !is_command && !is_ignored
def name: String = if (is_command) span.head.content else ""
- override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
+ override def toString =
+ if (is_command) name + "(" + id + ")"
+ else if (is_ignored) "<ignored>" else "<malformed>"
/* source text */
@@ -59,15 +64,17 @@
@volatile protected var state = new State(this)
def current_state: State = state
- private case class Consume(session: Session, message: XML.Tree)
+ private case class Consume(message: XML.Tree, forward: Command => Unit)
private case object Assign
private val accumulator = actor {
var assigned = false
loop {
react {
- case Consume(session: Session, message: XML.Tree) if !assigned =>
- state = state.+(session, message)
+ case Consume(message, forward) if !assigned =>
+ val old_state = state
+ state = old_state + message
+ if (!(state eq old_state)) forward(static_parent getOrElse this)
case Assign =>
assigned = true // single assignment
@@ -78,11 +85,14 @@
}
}
- def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
+ def consume(message: XML.Tree, forward: Command => Unit)
+ {
+ accumulator ! Consume(message, forward)
+ }
def assign_state(state_id: Isar_Document.State_ID): Command =
{
- val cmd = new Command(state_id, span)
+ val cmd = new Command(state_id, span, Some(this))
accumulator !? Assign
cmd.state = current_state
cmd
--- a/src/Pure/PIDE/state.scala Wed May 26 18:19:36 2010 +0200
+++ b/src/Pure/PIDE/state.scala Thu May 27 00:47:15 2010 +0200
@@ -70,50 +70,45 @@
/* message dispatch */
- def + (session: Session, message: XML.Tree): State =
- {
- val changed: State =
- message match {
- case XML.Elem(Markup.STATUS, _, elems) =>
- (this /: elems)((state, elem) =>
- elem match {
- case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
- case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
- case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
- case XML.Elem(kind, atts, body) =>
- atts match {
- case Position.Range(begin, end) =>
- if (kind == Markup.ML_TYPING) {
- val info = Pretty.string_of(body, margin = 40)
- state.add_markup(
- command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
+ def + (message: XML.Tree): State =
+ message match {
+ case XML.Elem(Markup.STATUS, _, elems) =>
+ (this /: elems)((state, elem) =>
+ elem match {
+ case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
+ case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
+ case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
+ case XML.Elem(kind, atts, body) =>
+ atts match {
+ case Position.Range(begin, end) =>
+ if (kind == Markup.ML_TYPING) {
+ val info = Pretty.string_of(body, margin = 40)
+ state.add_markup(
+ command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
+ }
+ else if (kind == Markup.ML_REF) {
+ body match {
+ case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
+ state.add_markup(command.markup_node(
+ begin - 1, end - 1,
+ Command.RefInfo(
+ Position.get_file(atts),
+ Position.get_line(atts),
+ Position.get_id(atts),
+ Position.get_offset(atts))))
+ case _ => state
}
- else if (kind == Markup.ML_REF) {
- body match {
- case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
- state.add_markup(command.markup_node(
- begin - 1, end - 1,
- Command.RefInfo(
- Position.get_file(atts),
- Position.get_line(atts),
- Position.get_id(atts),
- Position.get_offset(atts))))
- case _ => state
- }
- }
- else {
- state.add_markup(
- command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
- }
- case _ => state
- }
- case _ =>
- System.err.println("ignored status report: " + elem)
- state
- })
- case _ => add_result(message)
- }
- if (!(this eq changed)) session.command_change.event(command)
- changed
- }
+ }
+ else {
+ state.add_markup(
+ command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
+ }
+ case _ => state
+ }
+ case _ =>
+ System.err.println("ignored status report: " + elem)
+ state
+ })
+ case _ => add_result(message)
+ }
}
--- a/src/Pure/System/session.scala Wed May 26 18:19:36 2010 +0200
+++ b/src/Pure/System/session.scala Thu May 27 00:47:15 2010 +0200
@@ -25,7 +25,7 @@
trait Entity
{
val id: Entity_ID
- def consume(session: Session, message: XML.Tree): Unit
+ def consume(message: XML.Tree, forward: Command => Unit): Unit
}
}
@@ -37,9 +37,7 @@
val global_settings = new Event_Bus[Session.Global_Settings.type]
val raw_results = new Event_Bus[Isabelle_Process.Result]
val raw_output = new Event_Bus[Isabelle_Process.Result]
- val results = new Event_Bus[Command]
-
- val command_change = new Event_Bus[Command]
+ val commands_changed = new Event_Bus[Command_Set]
/* unique ids */
@@ -66,7 +64,7 @@
private case object Stop
private case class Begin_Document(path: String)
- private val session_actor = actor {
+ private lazy val session_actor = actor {
var prover: Isabelle_Process with Isar_Document = null
@@ -118,7 +116,7 @@
case None => None
case Some(id) => lookup_entity(id)
}
- if (target.isDefined) target.get.consume(this, result.message)
+ if (target.isDefined) target.get.consume(result.message, indicate_command_change)
else if (result.kind == Isabelle_Process.Kind.STATUS) {
// global status message
result.body match {
@@ -239,6 +237,52 @@
}
+
+ /** buffered command changes -- delay_first discipline **/
+
+ private lazy val command_change_buffer = actor {
+ import scala.compat.Platform.currentTime
+
+ var changed: Set[Command] = Set()
+ var flush_time: Option[Long] = None
+
+ def flush_timeout: Long =
+ flush_time match {
+ case None => 5000L
+ case Some(time) => (time - currentTime) max 0
+ }
+
+ def flush()
+ {
+ if (!changed.isEmpty) commands_changed.event(Command_Set(changed))
+ changed = Set()
+ flush_time = None
+ }
+
+ def invoke()
+ {
+ val now = currentTime
+ flush_time match {
+ case None => flush_time = Some(now + 100)
+ case Some(time) => if (now >= time) flush()
+ }
+ }
+
+ loop {
+ reactWithin(flush_timeout) {
+ case command: Command => changed += command; invoke()
+ case TIMEOUT => flush()
+ case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ def indicate_command_change(command: Command)
+ {
+ command_change_buffer ! command
+ }
+
+
/* main methods */
def start(timeout: Int, args: List[String]): Option[String] =
--- a/src/Tools/jEdit/src/jedit/document_view.scala Wed May 26 18:19:36 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu May 27 00:47:15 2010 +0200
@@ -69,7 +69,7 @@
}
-class Document_View(model: Document_Model, text_area: TextArea)
+class Document_View(val model: Document_Model, text_area: TextArea)
{
private val session = model.session
@@ -79,38 +79,22 @@
@volatile private var document = model.recent_document()
- /* buffer of changed commands -- owned by Swing thread */
-
- @volatile private var changed_commands: Set[Command] = Set()
+ /* commands_changed_actor */
- private val changed_delay = Swing_Thread.delay_first(100) {
- if (!changed_commands.isEmpty) {
- document = model.recent_document()
- for (cmd <- changed_commands if document.commands.contains(cmd)) { // FIXME cover doc states as well!!?
- update_syntax(cmd)
- invalidate_line(cmd)
- overview.repaint()
- }
- changed_commands = Set()
- }
- }
-
-
- /* command change actor */
-
- private case object Exit
-
- private val command_change_actor = actor {
+ private val commands_changed_actor = actor {
loop {
react {
- case command: Command => // FIXME rough filtering according to document family!?
+ case Command_Set(changed) =>
Swing_Thread.now {
- changed_commands += command
- changed_delay()
+ document = model.recent_document()
+ // FIXME cover doc states as well!!?
+ for (command <- changed if document.commands.contains(command)) {
+ update_syntax(command)
+ invalidate_line(command)
+ overview.repaint()
+ }
}
- case Exit => reply(()); exit()
-
case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
}
}
@@ -153,24 +137,23 @@
}
- /* caret_listener */
+ /* caret handling */
- private var _selected_command: Command = null
- private def selected_command = _selected_command
- private def selected_command_=(cmd: Command)
- {
- _selected_command = cmd
- session.results.event(cmd)
- }
+ def selected_command: Option[Command] =
+ document.command_at(text_area.getCaretPosition) match {
+ case Some((command, _)) => Some(command)
+ case None => None
+ }
private val caret_listener = new CaretListener
{
+ private var last_selected_command: Option[Command] = None
override def caretUpdate(e: CaretEvent)
{
- document.command_at(e.getDot) match {
- case Some((command, command_start)) if (selected_command != command) =>
- selected_command = command
- case _ =>
+ val selected = selected_command
+ if (selected != last_selected_command) {
+ last_selected_command = selected
+ if (selected.isDefined) session.indicate_command_change(selected.get)
}
}
}
@@ -192,9 +175,6 @@
{
val (start, stop) = model.lines_of_command(document, cmd)
text_area.invalidateLineRange(start, stop)
-
- if (selected_command == cmd)
- session.results.event(cmd)
}
private def invalidate_all() =
@@ -289,13 +269,12 @@
addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
text_area.addCaretListener(caret_listener)
text_area.addLeftOfScrollBar(overview)
- session.command_change += command_change_actor
+ session.commands_changed += commands_changed_actor
}
private def deactivate()
{
- session.command_change -= command_change_actor
- command_change_actor !? Exit
+ session.commands_changed -= commands_changed_actor
text_area.removeLeftOfScrollBar(overview)
text_area.removeCaretListener(caret_listener)
text_area.getPainter.removeExtension(text_area_extension)
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Wed May 26 18:19:36 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Thu May 27 00:47:15 2010 +0200
@@ -99,13 +99,19 @@
case Session.Global_Settings => handle_resize()
case Render(body) => html_panel.render(body)
- case cmd: Command =>
+ case Command_Set(changed) =>
Swing_Thread.now {
- if (follow.selected) Document_Model(view.getBuffer) else None
- } match {
- case None =>
- case Some(model) =>
- html_panel.render(filtered_results(model.recent_document, cmd))
+ if (follow.selected) {
+ Document_View(view.getTextArea) match {
+ case Some(doc_view) =>
+ doc_view.selected_command match {
+ case Some(cmd) if changed.contains(cmd) =>
+ html_panel.render(filtered_results(doc_view.model.recent_document, cmd))
+ case _ =>
+ }
+ case None =>
+ }
+ }
}
case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
@@ -115,13 +121,13 @@
override def init()
{
- Isabelle.session.results += main_actor
+ Isabelle.session.commands_changed += main_actor
Isabelle.session.global_settings += main_actor
}
override def exit()
{
- Isabelle.session.results -= main_actor
+ Isabelle.session.commands_changed -= main_actor
Isabelle.session.global_settings -= main_actor
}