diff options
| author |  wuestholz <unknown> | 2013-08-01 10:04:00 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-08-01 10:04:00 -0700 |
| commit | 0ce2ef03979ae45ccc9ce8a77802ba7031fc8270 (patch) | |
| tree | a0cc8dfcf1319dfc57347de24431f0adde7e927e /Source/DafnyExtension | |
| parent | 4a8977c741a668890f6095c2ff93a18175508746 (diff) | |
DafnyExtension: Made it select the last error state by default when an error is selected.
Diffstat (limited to 'Source/DafnyExtension')
| -rw-r--r-- | Source/DafnyExtension/ErrorModelTagger.cs | 15 | ||||
| -rw-r--r-- | Source/DafnyExtension/ResolverTagger.cs | 5 |
2 files changed, 14 insertions, 6 deletions
diff --git a/Source/DafnyExtension/ErrorModelTagger.cs b/Source/DafnyExtension/ErrorModelTagger.cs index 781814b2..7cef93fb 100644 --- a/Source/DafnyExtension/ErrorModelTagger.cs +++ b/Source/DafnyExtension/ErrorModelTagger.cs @@ -164,6 +164,13 @@ namespace DafnyLanguage esrtag.Error.StateChangeEvent += new DafnyError.StateChangeEventHandler((o) =>
{
result.Visibility = esrtag.Error.IsSelected ? System.Windows.Visibility.Visible : System.Windows.Visibility.Collapsed;
+ var isSelected = esrtag.Error.IsSelected && esrtag.Error.SelectedStateId == esrtag.Id;
+ result.Stroke = isSelected ? Brushes.Black : Brushes.DodgerBlue;
+ result.ToolTip = isSelected ? "unselect state" : "select state";
+ if (isSelected)
+ {
+ esrtag.Error.SelectedStateAdornment = result;
+ }
});
result.MouseDown += new MouseButtonEventHandler((s, e) =>
@@ -240,10 +247,16 @@ namespace DafnyLanguage // select the new one
ertag.Error.SelectedError = ertag.Error;
- ertag.Error.SelectedError.Notify();
ertag.Error.Adornment = result;
ertag.Error.Adornment.Stroke = Brushes.Black;
ertag.Error.Adornment.ToolTip = "unselect error";
+ if (!string.IsNullOrEmpty(ertag.Error.Model))
+ {
+ // select the last error state
+ ertag.Error.SelectedStateId = ertag.Error.StateSpans.Count() - 1;
+ DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(ertag.Error.Model, ertag.Error.SelectedStateId);
+ }
+ ertag.Error.SelectedError.Notify();
}
});
return result;
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs index dedf506a..230f79c5 100644 --- a/Source/DafnyExtension/ResolverTagger.cs +++ b/Source/DafnyExtension/ResolverTagger.cs @@ -376,11 +376,6 @@ namespace DafnyLanguage task.Navigate += new EventHandler(NavigateHandler);
}
_errorProvider.Tasks.Add(task);
-
- if (err.Model != null)
- {
-
- }
}
_errorProvider.ResumeRefresh();
}
|