summaryrefslogtreecommitdiff
path: root/Source/DafnyExtension
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2013-08-03 18:05:42 -0700
committerGravatar wuestholz <unknown>2013-08-03 18:05:42 -0700
commit04026edf3d0e905362a51995f246d3c2c0807c81 (patch)
tree1fa51be1d7095f4f19437e01113b12f5e5027db1 /Source/DafnyExtension
parent8af0f2d97ab5ca1a212c7f4901c43059ccb08e36 (diff)
DafnyExtension: Did some refactoring and added a description to error states.
Diffstat (limited to 'Source/DafnyExtension')
-rw-r--r--Source/DafnyExtension/ErrorModelTagger.cs41
-rw-r--r--Source/DafnyExtension/MenuProxy.cs8
-rw-r--r--Source/DafnyExtension/ResolverTagger.cs82
3 files changed, 76 insertions, 55 deletions
diff --git a/Source/DafnyExtension/ErrorModelTagger.cs b/Source/DafnyExtension/ErrorModelTagger.cs
index 76b0c10d..5fab67f3 100644
--- a/Source/DafnyExtension/ErrorModelTagger.cs
+++ b/Source/DafnyExtension/ErrorModelTagger.cs
@@ -86,7 +86,7 @@ namespace DafnyLanguage
foreach (var tag in _aggregator.GetTags(spans))
{
var ertag = tag.Tag as DafnyErrorResolverTag;
- if (ertag != null && ertag.Error.Model != null)
+ if (ertag != null && ertag.Error.ModelText != null)
{
NormalizedSnapshotSpanCollection normSpans = tag.Span.GetSpans(snapshot);
@@ -147,6 +147,11 @@ namespace DafnyLanguage
}
}
+ private static string ErrorStateToolTip(bool isSelected, string description)
+ {
+ return string.Format("{0}{1}", isSelected ? "unselect state" : "select state", !string.IsNullOrEmpty(description) ? " [" + description + "]" : "");
+ }
+
private static Ellipse CreateErrorStateAdornment(DafnyErrorStateResolverTag esrtag)
{
var result = new Ellipse
@@ -154,7 +159,7 @@ namespace DafnyLanguage
Fill = Brushes.DodgerBlue,
Height = 12.0,
Width = 12.0,
- ToolTip = "select state",
+ ToolTip = ErrorStateToolTip(false, esrtag.Description),
StrokeThickness = 3.0,
Stroke = Brushes.DodgerBlue,
Cursor = Cursors.Arrow,
@@ -166,9 +171,9 @@ namespace DafnyLanguage
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)
{
+ result.ToolTip = ErrorStateToolTip(isSelected, esrtag.Description);
esrtag.Error.SelectedStateAdornment = result;
}
});
@@ -182,7 +187,7 @@ namespace DafnyLanguage
esrtag.Error.SelectedStateAdornment = null;
esrtag.Error.SelectedStateId = -1;
result.Stroke = Brushes.DodgerBlue;
- result.ToolTip = "select state";
+ result.ToolTip = result.ToolTip.ToString().Replace("unselect", "select");
}
else
{
@@ -190,7 +195,7 @@ namespace DafnyLanguage
if (esrtag.Error.SelectedStateAdornment != null)
{
esrtag.Error.SelectedStateAdornment.Stroke = Brushes.DodgerBlue;
- esrtag.Error.SelectedStateAdornment.ToolTip = "select state";
+ esrtag.Error.SelectedStateAdornment.ToolTip = esrtag.Error.SelectedStateAdornment.ToolTip.ToString().Replace("unselect", "select");
esrtag.Error.SelectedStateAdornment = null;
esrtag.Error.SelectedStateId = -1;
}
@@ -198,11 +203,11 @@ namespace DafnyLanguage
// select the new one
esrtag.Error.SelectedStateAdornment = result;
esrtag.Error.SelectedStateAdornment.Stroke = Brushes.Black;
- esrtag.Error.SelectedStateAdornment.ToolTip = "unselect state";
+ esrtag.Error.SelectedStateAdornment.ToolTip = ErrorStateToolTip(true, esrtag.Description);
esrtag.Error.SelectedStateId = esrtag.Id;
- if (!string.IsNullOrEmpty(esrtag.Error.Model))
+ if (!string.IsNullOrEmpty(esrtag.Error.ModelText))
{
- DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(esrtag.Error.Model, esrtag.Id);
+ DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(esrtag.Error.ModelText, esrtag.Id);
}
}
});
@@ -221,18 +226,20 @@ namespace DafnyLanguage
Stroke = Brushes.Crimson,
Cursor = Cursors.Arrow,
};
+
result.Measure(new Size(double.PositiveInfinity, double.PositiveInfinity));
result.MouseDown += new MouseButtonEventHandler((s, e) =>
{
if (ertag.Error.IsSelected)
{
// unselect it
- var selErr = ertag.Error.SelectedError;
- ertag.Error.SelectedError = null;
- ertag.Error.SelectedStateId = -1;
- selErr.Notify();
+ var selErr = ertag.Error.SelectedError;
+ selErr.SelectedStateId = -1;
+ selErr.SelectedStateAdornment = null;
+ ertag.Error.SelectedError = null;
result.Stroke = Brushes.Crimson;
result.ToolTip = "select error";
+ selErr.Notify();
}
else
{
@@ -240,9 +247,10 @@ namespace DafnyLanguage
if (ertag.Error.SelectedError != null)
{
var selErr = ertag.Error.SelectedError;
+ selErr.SelectedStateId = -1;
+ selErr.SelectedStateAdornment = null;
selErr.Adornment.Stroke = Brushes.Crimson;
selErr.Adornment.ToolTip = "select error";
- ertag.Error.SelectedStateId = -1;
ertag.Error.SelectedError = null;
selErr.Notify();
}
@@ -252,11 +260,12 @@ namespace DafnyLanguage
ertag.Error.Adornment = result;
ertag.Error.Adornment.Stroke = Brushes.Black;
ertag.Error.Adornment.ToolTip = "unselect error";
- if (!string.IsNullOrEmpty(ertag.Error.Model))
+ if (!string.IsNullOrEmpty(ertag.Error.ModelText))
{
// select the last error state
- ertag.Error.SelectedStateId = ertag.Error.StateSpans.Count() - 1;
- DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(ertag.Error.Model, ertag.Error.SelectedStateId);
+ ertag.Error.SelectedStateId = ertag.Error.Model.States.Count() - 1;
+ ertag.Error.SelectedStateAdornment = null;
+ DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(ertag.Error.ModelText, ertag.Error.SelectedStateId);
}
ertag.Error.SelectedError.Notify();
}
diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs
index fc0c0d1d..59afc448 100644
--- a/Source/DafnyExtension/MenuProxy.cs
+++ b/Source/DafnyExtension/MenuProxy.cs
@@ -85,7 +85,7 @@ namespace DafnyLanguage
return activeTextView != null
&& DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
&& resolver.Program != null
- && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.Model));
+ && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.ModelText));
}
public void ShowErrorModel(IWpfTextView activeTextView)
@@ -94,14 +94,14 @@ namespace DafnyLanguage
var show = activeTextView != null
&& DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
&& resolver.Program != null
- && resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));
+ && resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.ModelText));
if (show)
{
- var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));
+ var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.ModelText));
if (selectedError != null)
{
- DafnyMenuPackage.ShowErrorModelInBVD(selectedError.Model, selectedError.SelectedStateId);
+ DafnyMenuPackage.ShowErrorModelInBVD(selectedError.ModelText, selectedError.SelectedStateId);
}
}
}
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index b1187054..81346c77 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -96,11 +96,13 @@ namespace DafnyLanguage
public readonly DafnyError Error;
public readonly ITrackingSpan Span;
public readonly int Id;
- public DafnyErrorStateResolverTag(DafnyError error, ITrackingSpan span, int id)
+ public readonly string Description;
+ public DafnyErrorStateResolverTag(DafnyError error, ITrackingSpan span, int id, string description)
{
Error = error;
Span = span;
Id = id;
+ Description = description;
}
}
@@ -278,9 +280,12 @@ namespace DafnyLanguage
for (int i = 0; i < err.StateSpans.Length; i++)
{
var span = err.StateSpans[i];
+ var name = err.Model.States.ToArray()[i].Name;
+ var descStart = name.LastIndexOf(": ") + 2;
+ var description = 1 < descStart ? name.Substring(descStart) : "";
if (span != null)
{
- yield return new TagSpan<IDafnyResolverTag>(span.GetSpan(currentSnapshot), new DafnyErrorStateResolverTag(err, span, i));
+ yield return new TagSpan<IDafnyResolverTag>(span.GetSpan(currentSnapshot), new DafnyErrorStateResolverTag(err, span, i, description));
}
}
}
@@ -471,46 +476,53 @@ namespace DafnyLanguage
public readonly string Message;
protected readonly ITextSnapshot Snapshot;
public readonly ITrackingSpan Span;
- public readonly string Model;
- private ITrackingSpan[] _stateSpans;
- public ITrackingSpan[] StateSpans
+ public readonly string ModelText;
+ public Microsoft.Boogie.Model _model;
+ public Microsoft.Boogie.Model Model
{
get
{
- if (!string.IsNullOrEmpty(Model))
+ if (_model == null && !string.IsNullOrEmpty(ModelText))
{
- if (_stateSpans != null) { return _stateSpans; }
- var locRegex = new Regex(@"\((\d+),(\d+)\)");
- using (var rd = new StringReader(Model))
+ using (var rd = new StringReader(ModelText))
{
- var model = Microsoft.Boogie.Model.ParseModels(rd, null).ToArray();
- Contract.Assert(model.Length == 1);
- _stateSpans = model[0].States.Select(
- cs =>
- {
- var match = locRegex.Match(cs.Name);
- if (!match.Success)
- {
- return null;
- }
- else
- {
- var line = Math.Max(0, int.Parse(match.Groups[1].Value) - 1);
- var column = Math.Max(0, int.Parse(match.Groups[2].Value) - 1);
- var sLine = Snapshot.GetLineFromLineNumber(line);
- Contract.Assert(column <= sLine.Length);
- var sLength = Math.Max(0, Math.Min(sLine.Length - column, 0));
- return Snapshot.CreateTrackingSpan(sLine.Start + column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);
- }
- }
- ).ToArray();
- return _stateSpans;
+ var models = Microsoft.Boogie.Model.ParseModels(rd, null).ToArray();
+ Contract.Assert(models.Length == 1);
+ _model = models[0];
}
}
- else
- {
- return null;
+ return _model;
+ }
+ }
+ private ITrackingSpan[] _stateSpans;
+ public ITrackingSpan[] StateSpans
+ {
+ get
+ {
+ if (_stateSpans == null && Model != null)
+ {
+ var model = Model;
+ var locRegex = new Regex(@"\((\d+),(\d+)\)");
+ _stateSpans = model.States.Select(
+ cs =>
+ {
+ var match = locRegex.Match(cs.Name);
+ if (!match.Success)
+ {
+ return null;
+ }
+ else
+ {
+ var line = Math.Max(0, int.Parse(match.Groups[1].Value) - 1);
+ var column = Math.Max(0, int.Parse(match.Groups[2].Value) - 1);
+ var sLine = Snapshot.GetLineFromLineNumber(line);
+ Contract.Assert(column <= sLine.Length);
+ var sLength = Math.Max(0, Math.Min(sLine.Length - column, 0));
+ return Snapshot.CreateTrackingSpan(sLine.Start + column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);
+ }
+ }).ToArray();
}
+ return _stateSpans;
}
}
public int SelectedStateId { get; set; }
@@ -561,7 +573,7 @@ namespace DafnyLanguage
Contract.Assert(Column <= sLine.Length);
var sLength = Math.Max(0, Math.Min(sLine.Length - Column, 5));
Span = snapshot.CreateTrackingSpan(sLine.Start + Column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);
- Model = model;
+ ModelText = model;
_errorSelection = _errorSelectionSingleton;
SelectedStateId = -1;
}