From 04026edf3d0e905362a51995f246d3c2c0807c81 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Sat, 3 Aug 2013 18:05:42 -0700 Subject: DafnyExtension: Did some refactoring and added a description to error states. --- Source/DafnyExtension/ErrorModelTagger.cs | 41 ++++++++++------ Source/DafnyExtension/MenuProxy.cs | 8 +-- Source/DafnyExtension/ResolverTagger.cs | 82 ++++++++++++++++++------------- 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(span.GetSpan(currentSnapshot), new DafnyErrorStateResolverTag(err, span, i)); + yield return new TagSpan(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; } -- cgit v1.2.3 From f8f9ceb9d068ad05264c2df21ccecb5149a85d1e Mon Sep 17 00:00:00 2001 From: wuestholz Date: Sun, 4 Aug 2013 14:05:35 -0700 Subject: DafnyExtension: Fixed issue with visual elements being accessed by non-owning thread. --- Source/DafnyExtension/ErrorModelTagger.cs | 168 ++++++++++++++++-------------- 1 file changed, 90 insertions(+), 78 deletions(-) diff --git a/Source/DafnyExtension/ErrorModelTagger.cs b/Source/DafnyExtension/ErrorModelTagger.cs index 5fab67f3..9029f019 100644 --- a/Source/DafnyExtension/ErrorModelTagger.cs +++ b/Source/DafnyExtension/ErrorModelTagger.cs @@ -152,7 +152,7 @@ namespace DafnyLanguage return string.Format("{0}{1}", isSelected ? "unselect state" : "select state", !string.IsNullOrEmpty(description) ? " [" + description + "]" : ""); } - private static Ellipse CreateErrorStateAdornment(DafnyErrorStateResolverTag esrtag) + private Ellipse CreateErrorStateAdornment(DafnyErrorStateResolverTag esrtag) { var result = new Ellipse { @@ -168,53 +168,59 @@ 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; - if (isSelected) - { - result.ToolTip = ErrorStateToolTip(isSelected, esrtag.Description); - esrtag.Error.SelectedStateAdornment = result; - } + _view.VisualElement.Dispatcher.Invoke(() => + { + 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; + if (isSelected) + { + result.ToolTip = ErrorStateToolTip(isSelected, esrtag.Description); + esrtag.Error.SelectedStateAdornment = result; + } + }); }); result.MouseDown += new MouseButtonEventHandler((s, e) => { - if (!esrtag.Error.IsSelected) { return; } - if (esrtag.Error.SelectedStateAdornment == result) - { - // unselect it - esrtag.Error.SelectedStateAdornment = null; - esrtag.Error.SelectedStateId = -1; - result.Stroke = Brushes.DodgerBlue; - result.ToolTip = result.ToolTip.ToString().Replace("unselect", "select"); - } - else - { - // unselect the old one - if (esrtag.Error.SelectedStateAdornment != null) + _view.VisualElement.Dispatcher.Invoke(() => { - esrtag.Error.SelectedStateAdornment.Stroke = Brushes.DodgerBlue; - esrtag.Error.SelectedStateAdornment.ToolTip = esrtag.Error.SelectedStateAdornment.ToolTip.ToString().Replace("unselect", "select"); - esrtag.Error.SelectedStateAdornment = null; - esrtag.Error.SelectedStateId = -1; - } - - // select the new one - esrtag.Error.SelectedStateAdornment = result; - esrtag.Error.SelectedStateAdornment.Stroke = Brushes.Black; - esrtag.Error.SelectedStateAdornment.ToolTip = ErrorStateToolTip(true, esrtag.Description); - esrtag.Error.SelectedStateId = esrtag.Id; - if (!string.IsNullOrEmpty(esrtag.Error.ModelText)) - { - DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(esrtag.Error.ModelText, esrtag.Id); - } - } + if (!esrtag.Error.IsSelected) { return; } + if (esrtag.Error.SelectedStateAdornment == result) + { + // unselect it + esrtag.Error.SelectedStateAdornment = null; + esrtag.Error.SelectedStateId = -1; + result.Stroke = Brushes.DodgerBlue; + result.ToolTip = result.ToolTip.ToString().Replace("unselect", "select"); + } + else + { + // unselect the old one + if (esrtag.Error.SelectedStateAdornment != null) + { + esrtag.Error.SelectedStateAdornment.Stroke = Brushes.DodgerBlue; + esrtag.Error.SelectedStateAdornment.ToolTip = esrtag.Error.SelectedStateAdornment.ToolTip.ToString().Replace("unselect", "select"); + esrtag.Error.SelectedStateAdornment = null; + esrtag.Error.SelectedStateId = -1; + } + + // select the new one + esrtag.Error.SelectedStateAdornment = result; + esrtag.Error.SelectedStateAdornment.Stroke = Brushes.Black; + esrtag.Error.SelectedStateAdornment.ToolTip = ErrorStateToolTip(true, esrtag.Description); + esrtag.Error.SelectedStateId = esrtag.Id; + if (!string.IsNullOrEmpty(esrtag.Error.ModelText)) + { + DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(esrtag.Error.ModelText, esrtag.Id); + } + } + }); }); return result; } - private static Ellipse CreateErrorAdornment(DafnyErrorResolverTag ertag) + private Ellipse CreateErrorAdornment(DafnyErrorResolverTag ertag) { var result = new Ellipse { @@ -230,45 +236,48 @@ namespace DafnyLanguage 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; - selErr.SelectedStateId = -1; - selErr.SelectedStateAdornment = null; - ertag.Error.SelectedError = null; - result.Stroke = Brushes.Crimson; - result.ToolTip = "select error"; - selErr.Notify(); - } - else - { - // unselect the old one - if (ertag.Error.SelectedError != null) + _view.VisualElement.Dispatcher.Invoke(() => { - var selErr = ertag.Error.SelectedError; - selErr.SelectedStateId = -1; - selErr.SelectedStateAdornment = null; - selErr.Adornment.Stroke = Brushes.Crimson; - selErr.Adornment.ToolTip = "select error"; - ertag.Error.SelectedError = null; - selErr.Notify(); - } - - // select the new one - ertag.Error.SelectedError = ertag.Error; - ertag.Error.Adornment = result; - ertag.Error.Adornment.Stroke = Brushes.Black; - ertag.Error.Adornment.ToolTip = "unselect error"; - if (!string.IsNullOrEmpty(ertag.Error.ModelText)) - { - // select the last error state - 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(); - } + if (ertag.Error.IsSelected) + { + // unselect it + 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 + { + // unselect the old one + 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.SelectedError = null; + selErr.Notify(); + } + + // select the new one + ertag.Error.SelectedError = ertag.Error; + ertag.Error.Adornment = result; + ertag.Error.Adornment.Stroke = Brushes.Black; + ertag.Error.Adornment.ToolTip = "unselect error"; + if (!string.IsNullOrEmpty(ertag.Error.ModelText)) + { + // select the last error state + 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(); + } + }); }); return result; } @@ -284,7 +293,10 @@ namespace DafnyLanguage if (spans.Count > 0) { SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End); - chng(this, new SnapshotSpanEventArgs(span)); + _view.VisualElement.Dispatcher.Invoke(() => + { + chng(this, new SnapshotSpanEventArgs(span)); + }); } } } -- cgit v1.2.3 From 1d9dcf0358280de5e948948afb4d899b20aaa2f2 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Mon, 5 Aug 2013 20:08:22 -0700 Subject: DafnyExtension: Use the same version number as Dafny (unfortunately needs to be updated separately in the vsixmanifests). --- Source/DafnyExtension/DafnyExtension.csproj | 5 +++-- Source/DafnyExtension/Properties/AssemblyInfo.cs | 13 ------------- Source/DafnyExtension/source.extension.vsixmanifest | 2 +- Source/DafnyMenu/DafnyMenu.csproj | 1 + Source/DafnyMenu/Properties/AssemblyInfo.cs | 13 ------------- Source/DafnyMenu/source.extension.vsixmanifest | 2 +- 6 files changed, 6 insertions(+), 30 deletions(-) diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj index 31e344a1..bad5f4c2 100644 --- a/Source/DafnyExtension/DafnyExtension.csproj +++ b/Source/DafnyExtension/DafnyExtension.csproj @@ -1,4 +1,4 @@ - + 11.0 @@ -157,6 +157,7 @@ + @@ -199,4 +200,4 @@ copy /y "..\Binaries\DafnyRuntime.cs" "$(ProjectDir)" --> - \ No newline at end of file + diff --git a/Source/DafnyExtension/Properties/AssemblyInfo.cs b/Source/DafnyExtension/Properties/AssemblyInfo.cs index a9922c2f..02da8a8a 100644 --- a/Source/DafnyExtension/Properties/AssemblyInfo.cs +++ b/Source/DafnyExtension/Properties/AssemblyInfo.cs @@ -17,16 +17,3 @@ using System.Runtime.InteropServices; // to COM components. If you need to access a type in this assembly from // COM, set the ComVisible attribute to true on that type. [assembly: ComVisible(false)] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Build and Revision Numbers -// by using the '*' as shown below: -// [assembly: AssemblyVersion("1.0.*")] -[assembly: AssemblyVersion("1.0.0.0")] -[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/Source/DafnyExtension/source.extension.vsixmanifest b/Source/DafnyExtension/source.extension.vsixmanifest index 9fda1773..5654b6cd 100644 --- a/Source/DafnyExtension/source.extension.vsixmanifest +++ b/Source/DafnyExtension/source.extension.vsixmanifest @@ -1,7 +1,7 @@ - + DafnyLanguageMode This is a language mode for using the Dafny language inside Visual Studio. diff --git a/Source/DafnyMenu/DafnyMenu.csproj b/Source/DafnyMenu/DafnyMenu.csproj index 7e9fb302..a7679e04 100644 --- a/Source/DafnyMenu/DafnyMenu.csproj +++ b/Source/DafnyMenu/DafnyMenu.csproj @@ -106,6 +106,7 @@ + diff --git a/Source/DafnyMenu/Properties/AssemblyInfo.cs b/Source/DafnyMenu/Properties/AssemblyInfo.cs index b1a5687d..9ceb8360 100644 --- a/Source/DafnyMenu/Properties/AssemblyInfo.cs +++ b/Source/DafnyMenu/Properties/AssemblyInfo.cs @@ -17,16 +17,3 @@ using System.Runtime.InteropServices; [assembly: ComVisible(false)] [assembly: CLSCompliant(false)] [assembly: NeutralResourcesLanguage("en-US")] - -// Version information for an assembly consists of the following four values: -// -// Major Version -// Minor Version -// Build Number -// Revision -// -// You can specify all the values or you can default the Revision and Build Numbers -// by using the '*' as shown below: - -[assembly: AssemblyVersion("1.0.0.0")] -[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/Source/DafnyMenu/source.extension.vsixmanifest b/Source/DafnyMenu/source.extension.vsixmanifest index 2e21caed..3ddc722c 100644 --- a/Source/DafnyMenu/source.extension.vsixmanifest +++ b/Source/DafnyMenu/source.extension.vsixmanifest @@ -1,7 +1,7 @@  - + DafnyMenu This is a menu for interacting with Dafny. -- cgit v1.2.3 From 820054e4ea6e9b8ed28fc081cbee18640a607458 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Mon, 5 Aug 2013 20:17:45 -0700 Subject: Updated 'PrepareDafnyZip.bat'. --- Binaries/PrepareDafnyZip.bat | 6 ++++-- Source/DafnyExtension/DafnyExtension.csproj | 3 --- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/Binaries/PrepareDafnyZip.bat b/Binaries/PrepareDafnyZip.bat index 3aede819..83aab1a9 100644 --- a/Binaries/PrepareDafnyZip.bat +++ b/Binaries/PrepareDafnyZip.bat @@ -9,20 +9,22 @@ if not exist %DEST_DIR% mkdir %DEST_DIR% for %%f in ( AbsInt.dll AbsInt.pdb Basetypes.dll Basetypes.pdb - BVD.exe BVD.pdb CodeContractsExtender.dll CodeContractsExtender.pdb Core.dll Core.pdb Dafny.exe Dafny.pdb DafnyPipeline.dll DafnyPipeline.pdb DafnyPrelude.bpl DafnyRuntime.cs + Doomed.dll Doomed.pdb + ExecutionEngine.dll ExecutionEngine.pdb Graph.dll Graph.pdb + Houdini.dll Houdini.dll Model.dll Model.pdb ParserHelper.dll ParserHelper.pdb Provers.SMTLib.dll Provers.SMTLib.pdb UnivBackPred2.smt2 VCExpr.dll VCExpr.pdb VCGeneration.dll VCGeneration.pdb - ..\Source\DafnyExtension\bin\Debug\DafnyLanguageService.vsix + DafnyLanguageService.vsix ) do ( copy %%f %DEST_DIR% ) diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj index bad5f4c2..b9c95c85 100644 --- a/Source/DafnyExtension/DafnyExtension.csproj +++ b/Source/DafnyExtension/DafnyExtension.csproj @@ -80,9 +80,6 @@ ..\..\..\boogie\Binaries\Houdini.dll - - ..\..\..\boogie\Binaries\Graph.dll - ..\..\..\boogie\Binaries\Model.dll -- cgit v1.2.3