From 94eb01be99a3273796fe36e631740be1c69163f3 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 15 Aug 2012 22:34:57 -0700
Subject: DafnyExtension: improvements

---
 Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs | 11 -----------
 Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs      |  2 +-
 2 files changed, 1 insertion(+), 12 deletions(-)

(limited to 'Util')

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) {
-- 
cgit v1.2.3