diff options
author | Rustan Leino <leino@microsoft.com> | 2012-08-15 22:34:57 -0700 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2012-08-15 22:34:57 -0700 |
commit | 2689b133ef688bef01c5f8e5cbe67110c3b9384a (patch) | |
tree | bd09516239b32893bb69921a36104def173ed4d2 /Util | |
parent | 63bf9ace6d8400626e4374e392f8584e4428b93a (diff) |
DafnyExtension: improvements
Diffstat (limited to 'Util')
-rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs | 11 | ||||
-rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs | 2 |
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) {
|