diff options
Diffstat (limited to 'Source/DafnyExtension/ErrorModelTagger.cs')
| -rw-r--r-- | Source/DafnyExtension/ErrorModelTagger.cs | 21 |
1 files changed, 18 insertions, 3 deletions
diff --git a/Source/DafnyExtension/ErrorModelTagger.cs b/Source/DafnyExtension/ErrorModelTagger.cs index 781814b2..76b0c10d 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) =>
@@ -173,7 +180,7 @@ namespace DafnyLanguage {
// unselect it
esrtag.Error.SelectedStateAdornment = null;
- esrtag.Error.SelectedStateId = 0;
+ esrtag.Error.SelectedStateId = -1;
result.Stroke = Brushes.DodgerBlue;
result.ToolTip = "select state";
}
@@ -185,7 +192,7 @@ namespace DafnyLanguage esrtag.Error.SelectedStateAdornment.Stroke = Brushes.DodgerBlue;
esrtag.Error.SelectedStateAdornment.ToolTip = "select state";
esrtag.Error.SelectedStateAdornment = null;
- esrtag.Error.SelectedStateId = 0;
+ esrtag.Error.SelectedStateId = -1;
}
// select the new one
@@ -222,6 +229,7 @@ namespace DafnyLanguage // unselect it
var selErr = ertag.Error.SelectedError;
ertag.Error.SelectedError = null;
+ ertag.Error.SelectedStateId = -1;
selErr.Notify();
result.Stroke = Brushes.Crimson;
result.ToolTip = "select error";
@@ -234,16 +242,23 @@ namespace DafnyLanguage var selErr = ertag.Error.SelectedError;
selErr.Adornment.Stroke = Brushes.Crimson;
selErr.Adornment.ToolTip = "select error";
+ ertag.Error.SelectedStateId = -1;
ertag.Error.SelectedError = null;
selErr.Notify();
}
// 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;
|