--- 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
--- 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
}
--- 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