aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorMark Christiaens2010-09-28 06:58:10 (EDT)
committerKnut Wannheden2011-04-28 05:18:04 (EDT)
commitbf26dfb6085475f62b9eed5912fa128335c0d744 (patch)
tree97be697230b7f709eb70ea0e58a27678d3aed923
parent0302cc38e1f155fa80e6a56377477961dbbfdad5 (diff)
downloadorg.eclipse.xtext-bf26dfb6085475f62b9eed5912fa128335c0d744.zip
org.eclipse.xtext-bf26dfb6085475f62b9eed5912fa128335c0d744.tar.gz
org.eclipse.xtext-bf26dfb6085475f62b9eed5912fa128335c0d744.tar.bz2
New branch starting from fully asserted version.
-rw-r--r--plugins/org.eclipse.xtext.ui/src/org/eclipse/xtext/ui/editor/FastDamagerRepairer.java5
1 files changed, 4 insertions, 1 deletions
diff --git a/plugins/org.eclipse.xtext.ui/src/org/eclipse/xtext/ui/editor/FastDamagerRepairer.java b/plugins/org.eclipse.xtext.ui/src/org/eclipse/xtext/ui/editor/FastDamagerRepairer.java
index ea84baa..18917b3 100644
--- a/plugins/org.eclipse.xtext.ui/src/org/eclipse/xtext/ui/editor/FastDamagerRepairer.java
+++ b/plugins/org.eclipse.xtext.ui/src/org/eclipse/xtext/ui/editor/FastDamagerRepairer.java
@@ -75,7 +75,7 @@ public class FastDamagerRepairer extends AbstractDamagerRepairer {
}
}
- private boolean checkInvariant = false;
+ private boolean checkInvariant = true;
private List<TokenInfo> tokenInfos;
private IRegion previousRegion;
private DocumentEvent previousEvent;
@@ -209,6 +209,7 @@ public class FastDamagerRepairer extends AbstractDamagerRepairer {
if (token.getStartIndex() >= e.fOffset + e.fText.length()) {
if (tokenStartsAt + lengthDiff == token.getStartIndex() && tokenInfo.type == token.getType()
&& token.getStopIndex() - token.getStartIndex() + 1 == tokenInfo.length) {
+ assert tokenInfosCopy.equals(tokenInfos);
return new Region(regionOffset, token.getStartIndex() - regionOffset);
}
}
@@ -257,6 +258,8 @@ public class FastDamagerRepairer extends AbstractDamagerRepairer {
token = (CommonToken) source.nextToken();
}
}
+
+ assert tokenInfosCopy.equals(tokenInfos);
return new Region(regionOffset, regionLength);
}