# HG changeset patch
# User wenzelm
# Date 1274914035 -7200
# Node ID 4c83696b340e0869f3efa7774a5f782b87ba050a
# Parent  1b6a4d9f397aed6a9f527b8f564b3663fdc077fa
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);

diff -r 1b6a4d9f397a -r 4c83696b340e src/Pure/PIDE/command.scala
--- 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
diff -r 1b6a4d9f397a -r 4c83696b340e src/Pure/PIDE/state.scala
--- 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)
+    }
 }
diff -r 1b6a4d9f397a -r 4c83696b340e src/Pure/System/session.scala
--- 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] =
diff -r 1b6a4d9f397a -r 4c83696b340e src/Tools/jEdit/src/jedit/document_view.scala
--- 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)
diff -r 1b6a4d9f397a -r 4c83696b340e src/Tools/jEdit/src/jedit/output_dockable.scala
--- 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
   }