diff options
| author |  Rustan Leino <unknown> | 2014-02-06 18:01:46 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-06 18:01:46 -0800 |
| commit | ef277df91eba1e166f709332ca5573b896944c19 (patch) | |
| tree | 3dc6422520ac39f24e0a56f50baea448b54250cd /Source/DafnyExtension | |
| parent | d42da0312acad16b390b8e5d9962dcce0995660c (diff) | |
Fixed bug in DafnyExtension (hover text computation would crash if Translator had not been run).
Fixed duplicate hover text information for Lines of calc statements.
Diffstat (limited to 'Source/DafnyExtension')
| -rw-r--r-- | Source/DafnyExtension/IdentifierTagger.cs | 10 | ||||
| -rw-r--r-- | Source/DafnyExtension/TokenTagger.cs | 2 |
2 files changed, 11 insertions, 1 deletions
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs index f2961d63..962dec3c 100644 --- a/Source/DafnyExtension/IdentifierTagger.cs +++ b/Source/DafnyExtension/IdentifierTagger.cs @@ -312,6 +312,16 @@ namespace DafnyLanguage if (s.Mod.Expressions != null) {
s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false, module));
}
+ } else if (stmt is CalcStmt) {
+ var s = (CalcStmt)stmt;
+ // skip the last line, which is just a duplicate anyway
+ for (int i = 0; i < s.Lines.Count - 1; i++) {
+ ExprRegions(s.Lines[i], regions, module);
+ }
+ foreach (var ss in stmt.SubStatements) {
+ StatementRegions(ss, regions, module);
+ }
+ return;
}
foreach (var ee in stmt.SubExpressions) {
ExprRegions(ee, regions, module);
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs index 3999db1e..b17fe7db 100644 --- a/Source/DafnyExtension/TokenTagger.cs +++ b/Source/DafnyExtension/TokenTagger.cs @@ -44,7 +44,7 @@ namespace DafnyLanguage get
{
string text = FixedHoverText;
- if (Variable != null)
+ if (Variable != null && Variable.HasBeenAssignedUniqueName)
{
bool wasUpdated;
var value = DafnyClassifier.DafnyMenuPackage.TryToLookupValueInCurrentModel(Variable.UniqueName, out wasUpdated);
|