summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2013-08-01 10:04:00 -0700
committerGravatar wuestholz <unknown>2013-08-01 10:04:00 -0700
commit0ce2ef03979ae45ccc9ce8a77802ba7031fc8270 (patch)
treea0cc8dfcf1319dfc57347de24431f0adde7e927e
parent4a8977c741a668890f6095c2ff93a18175508746 (diff)
DafnyExtension: Made it select the last error state by default when an error is selected.
-rw-r--r--Source/DafnyExtension/ErrorModelTagger.cs15
-rw-r--r--Source/DafnyExtension/ResolverTagger.cs5
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();
}