Session: predefined real time parameters;
Document_View: delayed caret handling, for improved reactivity;
selected_command: proper_command_at ignores ignored commands;

--- a/src/Pure/PIDE/document.scala	Mon Jul 19 08:59:43 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Jul 19 22:19:18 2010 +0200
@@ -162,6 +162,12 @@
     if (range.hasNext) Some(range.next) else None
   }
 
+  def proper_command_at(i: Int): Option[Command] =
+    command_at(i) match {
+      case Some((command, _)) => commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
+      case None => None
+    }
+
 
   /* command state assignment */
 

--- a/src/Pure/System/session.scala	Mon Jul 19 08:59:43 2010 +0200
+++ b/src/Pure/System/session.scala	Mon Jul 19 22:19:18 2010 +0200
@@ -16,6 +16,7 @@
   /* events */
 
   case object Global_Settings
+  case object Perspective
 
 
   /* managed entities */
@@ -32,12 +33,25 @@
 
 class Session(system: Isabelle_System)
 {
+  /* real time parameters */  // FIXME properties or settings (!?)
+
+  // user input (e.g. text edits, cursor movement)
+  val input_delay = 300
+
+  // prover output (markup, common messages)
+  val output_delay = 100
+
+  // GUI layout updates
+  val update_delay = 500
+
+
   /* pervasive event buses */
 
   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 commands_changed = new Event_Bus[Command_Set]
+  val perspective = new Event_Bus[Session.Perspective.type]
 
 
   /* unique ids */
@@ -263,7 +277,7 @@
     {
       val now = currentTime
       flush_time match {
-        case None => flush_time = Some(now + 100)   // FIXME output_delay property
+        case None => flush_time = Some(now + output_delay)
         case Some(time) => if (now >= time) flush()
       }
     }

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Mon Jul 19 08:59:43 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Mon Jul 19 22:19:18 2010 +0200
@@ -100,7 +100,7 @@
 
   private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
 
-  private val edits_delay = Swing_Thread.delay_last(300) {  // FIXME input_delay property
+  private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
     if (!edits_buffer.isEmpty) {
       val new_change = current_change().edit(session, edits_buffer.toList)
       edits_buffer.clear

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Mon Jul 19 08:59:43 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Mon Jul 19 22:19:18 2010 +0200
@@ -211,23 +211,14 @@
 
   /* caret handling */
 
-  def selected_command: Option[Command] =
-    model.recent_document().command_at(text_area.getCaretPosition) match {
-      case Some((command, _)) => Some(command)
-      case None => None
-    }
+  def selected_command(): Option[Command] =
+    model.recent_document().proper_command_at(text_area.getCaretPosition)
 
-  private val caret_listener = new CaretListener
-  {
-    private var last_selected_command: Option[Command] = None
-    override def caretUpdate(e: CaretEvent)
-    {
-      val selected = selected_command
-      if (selected != last_selected_command) {
-        last_selected_command = selected
-        if (selected.isDefined) session.indicate_command_change(selected.get)
-      }
+  private val caret_listener = new CaretListener {
+    private val delay = Swing_Thread.delay_last(session.input_delay) {
+      session.perspective.event(Session.Perspective)
     }
+    override def caretUpdate(e: CaretEvent) { delay() }
   }
 
 

--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Jul 19 08:59:43 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Mon Jul 19 22:19:18 2010 +0200
@@ -46,20 +46,21 @@
     }
   }
 
-  private def handle_caret()
-  {
+  private def handle_perspective(): Boolean =
     Swing_Thread.now {
       Document_View(view.getTextArea) match {
-        case Some(doc_view) => current_command = doc_view.selected_command
-        case None =>
+        case Some(doc_view) =>
+          val cmd = doc_view.selected_command()
+          if (current_command == cmd) false
+          else { current_command = cmd; true }
+        case None => false
       }
     }
-  }
 
   private def handle_update(restriction: Option[Set[Command]] = None)
   {
     Swing_Thread.now {
-      if (follow_caret) handle_caret()
+      if (follow_caret) handle_perspective()
       Document_View(view.getTextArea) match {
         case Some(doc_view) =>
           current_command match {
@@ -87,6 +88,7 @@
       react {
         case Session.Global_Settings => handle_resize()
         case Command_Set(changed) => handle_update(Some(changed))
+        case Session.Perspective => if (handle_perspective()) handle_update()
         case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
       }
     }
@@ -94,21 +96,23 @@
 
   override def init()
   {
+    Isabelle.session.global_settings += main_actor
     Isabelle.session.commands_changed += main_actor
-    Isabelle.session.global_settings += main_actor
+    Isabelle.session.perspective += main_actor
   }
 
   override def exit()
   {
+    Isabelle.session.global_settings -= main_actor
     Isabelle.session.commands_changed -= main_actor
-    Isabelle.session.global_settings -= main_actor
+    Isabelle.session.perspective -= main_actor
   }
 
 
   /* resize */
 
   addComponentListener(new ComponentAdapter {
-    val delay = Swing_Thread.delay_last(500) { handle_resize() }  // FIXME update_delay property
+    val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
     override def componentResized(e: ComponentEvent) { delay() }
   })
 
@@ -138,7 +142,7 @@
   auto_update.tooltip = "Indicate automatic update following cursor movement"
 
   private val update = new Button("Update") {
-    reactions += { case ButtonClicked(_) => handle_caret(); handle_update() }
+    reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() }
   }
   update.tooltip = "Update display according to the command at cursor position"