diff options
| author |  Rustan Leino <unknown> | 2014-02-04 13:50:35 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-04 13:50:35 -0800 |
| commit | 350943135ec691291f194964098ac663356eb21f (patch) | |
| tree | 108f2fc26d11f4708983556fa57c12aab69f9486 /Source/DafnyExtension/IdentifierTagger.cs | |
| parent | cec5d3c3de15389f7dab83013a57c6a586fab4a4 (diff) | |
Mark auto-generated expressions (in "decreases" clauses) and don't use these when figuring out hover text.
Diffstat (limited to 'Source/DafnyExtension/IdentifierTagger.cs')
| -rw-r--r-- | Source/DafnyExtension/IdentifierTagger.cs | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs index d459d7eb..f2961d63 100644 --- a/Source/DafnyExtension/IdentifierTagger.cs +++ b/Source/DafnyExtension/IdentifierTagger.cs @@ -237,7 +237,10 @@ namespace DafnyLanguage static void ExprRegions(Microsoft.Dafny.Expression expr, List<IdRegion> regions, ModuleDefinition module) {
Contract.Requires(expr != null);
Contract.Requires(regions != null);
- if (expr is IdentifierExpr) {
+ if (expr is AutoGeneratedExpression) {
+ // do nothing
+ return;
+ } else if (expr is IdentifierExpr) {
var e = (IdentifierExpr)expr;
IdRegion.Add(regions, e.tok, e.Var, false, module);
} else if (expr is FieldSelectExpr) {
|