# HG changeset patch
# User immler@in.tum.de
# Date 1243429009 -7200
# Node ID d68352286c9131344251581a2e0d2e3fc4a3a38e
# Parent  daa397b6401ce9e4659ced8f0904312315f41055
split large changes for faster responses of prover

diff -r daa397b6401c -r d68352286c91 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon May 25 14:36:40 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed May 27 14:56:49 2009 +0200
@@ -26,6 +26,8 @@
 
 object TheoryView {
 
+  val MAX_CHANGE_LENGTH = 1500
+  
   def choose_color(state: Command): Color = {
     if (state == null) Color.red
     else
@@ -220,8 +222,15 @@
 
   private def commit: Unit = synchronized {
     if (col != null) {
-      changes = col :: changes
-      document_actor ! col
+      def split_changes(c: Text.Change): List[Text.Change] = {
+        val MCL = TheoryView.MAX_CHANGE_LENGTH
+        if (c.added.length <= MCL) List(c)
+        else Text.Change(c.id, c.start, c.added.substring(0, MCL), c.removed) ::
+          split_changes(new Text.Change(id(), c.start + MCL, c.added.substring(MCL), c.removed))
+      }
+      val new_changes = split_changes(col)
+      changes = new_changes.reverse ::: changes
+      new_changes map (document_actor ! _)
     }
     col = null
     if (col_timer.isRunning())