# HG changeset patch
# User immler@in.tum.de
# Date 1243962058 -7200
# Node ID cf37a9f988bf8445815cf0070778f0c936204e12
# Parent  b17ebec3690c202e60f29d1d9dc6b395321d3d88
ignore unchanged commands

diff -r b17ebec3690c -r cf37a9f988bf src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jun 02 19:00:58 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jun 02 19:00:58 2009 +0200
@@ -154,21 +154,29 @@
                             new_tokenset: LinearSet[Token],
                             new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) =
   {
-    val cmd_first_changed =
-      if (before_change.isDefined) commands.find(_.tokens.contains(before_change.get))
-      else None
-    val cmd_last_changed =
-      if (after_change.isDefined) commands.find(_.tokens.contains(after_change.get))
-      else None
+    val cmd_before_change = before_change match {
+      case None => None
+      case Some(bc) =>
+        val cmd_with_bc = commands.find(_.contains(bc)).get
+        if (cmd_with_bc.tokens.last == bc) {
+          if (new_tokenset.next(bc).map(_.is_start).getOrElse(true))
+            Some(cmd_with_bc)
+          else commands.prev(cmd_with_bc)
+        }
+        else commands.prev(cmd_with_bc)
+    }
 
-    val cmd_before_change =
-      if (cmd_first_changed.isDefined) commands.prev(cmd_first_changed.get)
-      else None
-    val cmd_after_change =
-      if (cmd_last_changed.isDefined) commands.next(cmd_last_changed.get)
-      else None
+    val cmd_after_change = after_change match {
+      case None => None
+      case Some(ac) =>
+        val cmd_with_ac = commands.find(_.contains(ac)).get
+        if (ac.is_start)
+          Some(cmd_with_ac)
+        else
+          commands.next(cmd_with_ac)
+    }
 
-    val removed_commands = commands.dropWhile(Some(_) != cmd_first_changed).
+    val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1).
       takeWhile(Some(_) != cmd_after_change)
 
     // calculate inserted commands
@@ -181,19 +189,30 @@
       }
     }
 
-    val split_begin_tokens =
-      if (!cmd_first_changed.isDefined || !before_change.isDefined) Nil
-      else {
-        cmd_first_changed.get.tokens.takeWhile(_ != before_change.get) ::: List(before_change.get)
-      }
-    val split_end_tokens =
-      if (!cmd_last_changed.isDefined || !after_change.isDefined) Nil
-      else {
-        cmd_last_changed.get.tokens.dropWhile(_ != after_change.get)
-      }
+    val split_begin =
+      if (before_change.isDefined) {
+        val changed =
+          if (cmd_before_change.isDefined)
+            new_tokenset.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1)
+          else new_tokenset
+        if (changed.exists(_ == before_change.get))
+          changed.takeWhile(_ != before_change.get).toList ::: List(before_change.get)
+        else Nil
+      } else Nil
 
-    val rescanning_tokens = split_begin_tokens ::: inserted_tokens ::: split_end_tokens
-    val inserted_commands = tokens_to_commands(rescanning_tokens)
+    val split_end =
+      if (after_change.isDefined && cmd_after_change.isDefined) {
+        val unchanged = new_tokenset.dropWhile(_ != after_change.get)
+        if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
+          unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
+        else Nil
+      } else Nil
+
+    val rescan_begin = split_begin ::: before_change.map(bc => new_tokenset.dropWhile(_ != bc).drop(1)).
+      getOrElse(new_tokenset).toList
+    val rescanning_tokens = after_change.map(ac => rescan_begin.takeWhile(_ != ac)).
+      getOrElse(rescan_begin) ::: split_end
+    val inserted_commands = tokens_to_commands(rescanning_tokens.toList)
 
     val change = new StructureChange(cmd_before_change, inserted_commands, removed_commands.toList)
     // build new document
diff -r b17ebec3690c -r cf37a9f988bf src/Tools/jEdit/src/proofdocument/Token.scala
--- a/src/Tools/jEdit/src/proofdocument/Token.scala	Tue Jun 02 19:00:58 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Tue Jun 02 19:00:58 2009 +0200
@@ -37,6 +37,8 @@
 }
 
 class Token(val content: String, val kind: Token.Kind.Value) {
+  import Token.Kind._
   val length = content.length
   override def toString = content
+  val is_start = kind == COMMAND_START || kind == COMMENT
 }
diff -r b17ebec3690c -r cf37a9f988bf src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Tue Jun 02 19:00:58 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Tue Jun 02 19:00:58 2009 +0200
@@ -43,6 +43,8 @@
   def start(doc: ProofDocument) = doc.token_start(tokens.first)
   def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
 
+  def contains(p: Token) = tokens.contains(p)
+
   /* command status */
 
   var state_id: IsarDocument.State_ID = null