postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;

--- a/src/Pure/System/session.scala	Fri Sep 07 13:58:54 2012 +0200
+++ b/src/Pure/System/session.scala	Fri Sep 07 15:00:03 2012 +0200
@@ -24,6 +24,7 @@
   //{{{
   case object Global_Settings
   case object Caret_Focus
+  case class Raw_Edits(edits: List[Document.Edit_Text])
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
@@ -61,6 +62,7 @@
 
   val global_settings = new Event_Bus[Session.Global_Settings.type]
   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[Isabelle_Process.Output]
@@ -168,7 +170,6 @@
 
   private case class Start(args: List[String])
   private case object Cancel_Execution
-  private case class Edit(edits: List[Document.Edit_Text])
   private case class Change(
     doc_edits: List[Document.Edit_Command],
     previous: Document.Version,
@@ -391,12 +392,13 @@
         case Cancel_Execution if prover.isDefined =>
           prover.get.cancel_execution()
 
-        case Edit(edits) if prover.isDefined =>
+        case raw @ Session.Raw_Edits(edits) if prover.isDefined =>
           prover.get.discontinue_execution()
 
           val previous = global_state().history.tip.version
           val version = Future.promise[Document.Version]
           val change = global_state >>> (_.continue_history(previous, edits, version))
+          raw_edits.event(raw)
           change_parser ! Text_Edits(previous, edits, version)
 
           reply(())
@@ -435,7 +437,7 @@
   def cancel_execution() { session_actor ! Cancel_Execution }
 
   def edit(edits: List[Document.Edit_Text])
-  { session_actor !? Edit(edits) }
+  { session_actor !? Session.Raw_Edits(edits) }
 
   def init_node(name: Document.Node.Name,
     header: Document.Node.Header, perspective: Text.Perspective, text: String)

--- a/src/Pure/System/swing_thread.scala	Fri Sep 07 13:58:54 2012 +0200
+++ b/src/Pure/System/swing_thread.scala	Fri Sep 07 15:00:03 2012 +0200
@@ -51,6 +51,7 @@
   {
     def invoke(): Unit
     def revoke(): Unit
+    def postpone(time: Time): Unit
   }
 
   private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Delay =
@@ -77,6 +78,15 @@
         timer.stop()
         timer.setDelay(time.ms.toInt)
       }
+
+      def postpone(alt_time: Time)
+      {
+        require()
+        if (timer.isRunning) {
+          timer.setDelay(timer.getDelay max alt_time.ms.toInt)
+          timer.restart()
+        }
+      }
     }
 
   // delayed action after first invocation

--- a/src/Tools/jEdit/src/document_view.scala	Fri Sep 07 13:58:54 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Fri Sep 07 15:00:03 2012 +0200
@@ -364,6 +364,11 @@
   private val main_actor = actor {
     loop {
       react {
+        case _: Session.Raw_Edits =>
+          Swing_Thread.later {
+            overview.delay_repaint.postpone(Isabelle.session.input_delay)
+          }
+
         case changed: Session.Commands_Changed =>
           val buffer = model.buffer
           Swing_Thread.later {
@@ -374,7 +379,7 @@
                 if (changed.assignment ||
                     (changed.nodes.contains(model.name) &&
                      changed.commands.exists(snapshot.node.commands.contains)))
-                  overview.delay_repaint.invoke()
+                  Swing_Thread.later { overview.delay_repaint.invoke() }
 
                 visible_range() match {
                   case Some(visible) =>
@@ -422,6 +427,7 @@
     painter.addMouseMotionListener(mouse_motion_listener)
     text_area.addCaretListener(caret_listener)
     text_area.addLeftOfScrollBar(overview)
+    session.raw_edits += main_actor
     session.commands_changed += main_actor
     session.global_settings += main_actor
   }
@@ -429,6 +435,7 @@
   private def deactivate()
   {
     val painter = text_area.getPainter
+    session.raw_edits -= main_actor
     session.commands_changed -= main_actor
     session.global_settings -= main_actor
     text_area.removeFocusListener(focus_listener)