summaryrefslogtreecommitdiff
path: root/Util
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2012-08-15 22:34:57 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2012-08-15 22:34:57 -0700
commit2689b133ef688bef01c5f8e5cbe67110c3b9384a (patch)
treebd09516239b32893bb69921a36104def173ed4d2 /Util
parent63bf9ace6d8400626e4374e392f8584e4428b93a (diff)
DafnyExtension: improvements
Diffstat (limited to 'Util')
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs11
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs2
2 files changed, 1 insertions, 12 deletions
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
index 77a1fcf8..0304dd20 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
@@ -114,9 +114,6 @@ namespace DafnyLanguage
foreach (var module in program.Modules) {
foreach (var d in module.TopLevelDecls) {
- if (!HasBodyTokens(d) && !(d is ClassDecl)) {
- continue;
- }
if (d is DatatypeDecl) {
var dt = (DatatypeDecl)d;
foreach (var ctor in dt.Ctors) {
@@ -129,9 +126,6 @@ namespace DafnyLanguage
} else if (d is ClassDecl) {
var cl = (ClassDecl)d;
foreach (var member in cl.Members) {
- if (!HasBodyTokens(member)) {
- continue;
- }
if (member is Function) {
var f = (Function)member;
foreach (var p in f.Formals) {
@@ -261,11 +255,6 @@ namespace DafnyLanguage
}
}
- bool HasBodyTokens(Declaration decl) {
- Contract.Requires(decl != null);
- return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken;
- }
-
class IdRegion
{
public readonly int Start;
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index c4ba346a..5853f180 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -220,7 +220,7 @@ namespace DafnyLanguage
}
// we have a keyword or an identifier
string s = txt.Substring(cur, end - cur);
- if (0 < trailingDigits && s.Length == 5 + trailingDigits && s.StartsWith("array") && s[5] != '0' && s != "array1") {
+ if (0 < trailingDigits && s.Length == 5 + trailingDigits && s.StartsWith("array") && s[5] != '0' && (trailingDigits != 1 || s[5] != '1')) {
// this is a keyword (array2, array3, ...)
} else {
switch (s) {