summaryrefslogtreecommitdiff
path: root/Source/DafnyExtension
diff options
context:
space:
mode:
Diffstat (limited to 'Source/DafnyExtension')
-rw-r--r--Source/DafnyExtension/BufferIdleEventUtil.cs2
-rw-r--r--Source/DafnyExtension/DafnyDriver.cs135
-rw-r--r--Source/DafnyExtension/DafnyExtension.csproj79
-rw-r--r--Source/DafnyExtension/IdentifierTagger.cs167
-rw-r--r--Source/DafnyExtension/MenuProxy.cs25
-rw-r--r--Source/DafnyExtension/OutliningTagger.cs30
-rw-r--r--Source/DafnyExtension/ProgressMargin.cs46
-rw-r--r--Source/DafnyExtension/ResolverTagger.cs140
-rw-r--r--Source/DafnyExtension/TokenTagger.cs214
-rw-r--r--Source/DafnyExtension/packages.config29
-rw-r--r--Source/DafnyExtension/source.extension.vsixmanifest5
11 files changed, 586 insertions, 286 deletions
diff --git a/Source/DafnyExtension/BufferIdleEventUtil.cs b/Source/DafnyExtension/BufferIdleEventUtil.cs
index 5ab9df09..8a1ad0ed 100644
--- a/Source/DafnyExtension/BufferIdleEventUtil.cs
+++ b/Source/DafnyExtension/BufferIdleEventUtil.cs
@@ -120,7 +120,7 @@ namespace DafnyLanguage
{
timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle)
{
- Interval = TimeSpan.FromMilliseconds(50)
+ Interval = TimeSpan.FromMilliseconds(500)
};
timer.Tick += (s, e) =>
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 5b8cc943..13b53a1b 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -1,6 +1,7 @@
using System;
using System.Collections.Concurrent;
using System.Collections.Generic;
+using System.Collections.ObjectModel;
using System.Diagnostics.Contracts;
using System.IO;
using System.Linq;
@@ -18,13 +19,16 @@ namespace DafnyLanguage
{
readonly string _filename;
readonly ITextSnapshot _snapshot;
+ readonly ITextBuffer _buffer;
Dafny.Program _program;
+ static object bufferDafnyKey = new object();
List<DafnyError> _errors = new List<DafnyError>();
public List<DafnyError> Errors { get { return _errors; } }
- public DafnyDriver(ITextSnapshot snapshot, string filename) {
- _snapshot = snapshot;
+ public DafnyDriver(ITextBuffer buffer, string filename) {
+ _buffer = buffer;
+ _snapshot = buffer.CurrentSnapshot;
_filename = filename;
}
@@ -37,9 +41,11 @@ namespace DafnyLanguage
if (Dafny.DafnyOptions.O == null) {
var options = new Dafny.DafnyOptions();
options.ProverKillTime = 10;
+ options.AutoTriggers = true;
options.ErrorTrace = 0;
options.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1);
options.ModelViewFile = "-";
+ options.UnicodeOutput = true;
Dafny.DafnyOptions.Install(options);
// Read additional options from DafnyOptions.txt
@@ -105,82 +111,84 @@ namespace DafnyLanguage
#region Parsing and type checking
- internal Dafny.Program ProcessResolution() {
- if (!ParseAndTypeCheck()) {
+ internal Dafny.Program ProcessResolution(bool runResolver) {
+ if (!ParseAndTypeCheck(runResolver)) {
return null;
}
return _program;
}
- bool ParseAndTypeCheck() {
- Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null);
- Dafny.BuiltIns builtIns = new Dafny.BuiltIns();
- Dafny.Errors parseErrors = new VSErrors(this);
- int errorCount = Dafny.Parser.Parse(_snapshot.GetText(), _filename, module, builtIns, parseErrors);
- string errString = Dafny.Main.ParseIncludes(module, builtIns, new List<string>(), parseErrors);
- if (errorCount != 0 || errString != null)
+ bool ParseAndTypeCheck(bool runResolver) {
+ Tuple<ITextSnapshot, Dafny.Program, List<DafnyError>> parseResult;
+ Dafny.Program program;
+ var errorReporter = new VSErrorReporter(this);
+ if (_buffer.Properties.TryGetProperty(bufferDafnyKey, out parseResult) &&
+ (parseResult.Item1 == _snapshot)) {
+ // already parsed;
+ program = parseResult.Item2;
+ _errors = parseResult.Item3;
+ if (program == null)
+ runResolver = false;
+ } else {
+ Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null);
+ Dafny.BuiltIns builtIns = new Dafny.BuiltIns();
+ var parseErrors = new Dafny.Errors(errorReporter);
+ int errorCount = Dafny.Parser.Parse(_snapshot.GetText(), _filename, _filename, module, builtIns, parseErrors);
+ string errString = Dafny.Main.ParseIncludes(module, builtIns, new List<string>(), parseErrors);
+
+ if (errorCount != 0 || errString != null) {
+ runResolver = false;
+ program = null;
+ } else {
+ program = new Dafny.Program(_filename, module, builtIns, errorReporter);
+ }
+ _buffer.Properties[bufferDafnyKey] = new Tuple<ITextSnapshot, Dafny.Program, List<DafnyError>>(_snapshot, program, _errors);
+ }
+ if (!runResolver) {
return false;
- Dafny.Program program = new Dafny.Program(_filename, module, builtIns);
+ }
- var r = new VSResolver(program, this);
+ var r = new Resolver(program);
r.ResolveProgram(program);
- if (r.ErrorCount != 0)
+ if (errorReporter.Count(ErrorLevel.Error) != 0)
return false;
- program.AdditionalInformation.AddRange(r.AdditionalInformation);
_program = program;
return true; // success
}
+
void RecordError(string filename, int line, int col, ErrorCategory cat, string msg, bool isRecycled = false)
{
- _errors.Add(new DafnyError(filename, line, col, cat, msg, _snapshot, isRecycled, null, System.IO.Path.GetFullPath(this._filename) == filename));
+ _errors.Add(new DafnyError(filename, line - 1, col - 1, cat, msg, _snapshot, isRecycled, null, System.IO.Path.GetFullPath(this._filename) == filename));
}
- class VSErrors : Dafny.Errors
+ class VSErrorReporter : Dafny.ErrorReporter
{
DafnyDriver dd;
- public VSErrors(DafnyDriver dd) {
- this.dd = dd;
- }
- public override void SynErr(string filename, int line, int col, string msg) {
- dd.RecordError(filename, line - 1, col - 1, ErrorCategory.ParseError, msg);
- count++;
- }
- public override void SemErr(string filename, int line, int col, string msg) {
- dd.RecordError(filename, line - 1, col - 1, ErrorCategory.ResolveError, msg);
- count++;
- }
- public override void Warning(string filename, int line, int col, string msg) {
- dd.RecordError(filename, line - 1, col - 1, ErrorCategory.ParseWarning, msg);
- }
- }
- class VSResolver : Dafny.Resolver
- {
- DafnyDriver dd;
- Dictionary<IToken, HashSet<AdditionalInformation>> _additionalInformation = new Dictionary<IToken, HashSet<AdditionalInformation>>();
- public List<AdditionalInformation> AdditionalInformation { get { return _additionalInformation.Values.SelectMany(i => i).ToList(); } }
-
- public VSResolver(Dafny.Program program, DafnyDriver dd)
- : base(program) {
+ public VSErrorReporter(DafnyDriver dd) {
this.dd = dd;
-
- AdditionalInformationReporter =
- (addinfo)
- =>
- {
- if (!_additionalInformation.ContainsKey(addinfo.Token)) {
- _additionalInformation.Add(addinfo.Token, new HashSet<AdditionalInformation>());
- }
- _additionalInformation[addinfo.Token].Add(addinfo);
- };
}
- public override void Error(Bpl.IToken tok, string msg, params object[] args) {
- string s = string.Format(msg, args);
- dd.RecordError(tok.filename, tok.line - 1, tok.col - 1, ErrorCategory.ResolveError, s);
- ErrorCount++;
+ // TODO: The error tracking could be made better to track the full information returned by Dafny
+ public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {
+ if (base.Message(source, level, tok, msg)) {
+ switch (level) {
+ case ErrorLevel.Error:
+ dd.RecordError(tok.filename, tok.line, tok.col, source == MessageSource.Parser ? ErrorCategory.ParseError : ErrorCategory.ResolveError, msg);
+ break;
+ case ErrorLevel.Warning:
+ dd.RecordError(tok.filename, tok.line, tok.col, source == MessageSource.Parser ? ErrorCategory.ParseWarning : ErrorCategory.ResolveWarning, msg);
+ break;
+ case ErrorLevel.Info:
+ // The AllMessages variable already keeps track of this
+ break;
+ }
+ return true;
+ } else {
+ return false;
+ }
}
}
@@ -191,7 +199,10 @@ namespace DafnyLanguage
public static void Compile(Dafny.Program dafnyProgram, TextWriter outputWriter)
{
Microsoft.Dafny.DafnyOptions.O.SpillTargetCode = true;
- Microsoft.Dafny.DafnyDriver.CompileDafnyProgram(dafnyProgram, dafnyProgram.FullName, outputWriter);
+ // Currently there are no provisions for specifying other files to compile with from the
+ // VS interface, so just send an empty list.
+ ReadOnlyCollection<string> otherFileNames = new List<string>().AsReadOnly();
+ Microsoft.Dafny.DafnyDriver.CompileDafnyProgram(dafnyProgram, dafnyProgram.FullName, otherFileNames, outputWriter);
}
#endregion
@@ -239,6 +250,11 @@ namespace DafnyLanguage
return Dafny.DafnyOptions.Clo.VerifySnapshots;
}
+ public static void SetDiagnoseTimeouts(bool v)
+ {
+ Dafny.DafnyOptions.Clo.RunDiagnosticsOnTimeout = v;
+ }
+
public static int ChangeIncrementalVerification(int mode)
{
var old = Dafny.DafnyOptions.Clo.VerifySnapshots;
@@ -260,8 +276,15 @@ namespace DafnyLanguage
return Dafny.DafnyOptions.Clo.VerifySnapshots;
}
+ public static bool ChangeAutomaticInduction() {
+ var old = Dafny.DafnyOptions.O.Induction;
+ // toggle between modes 1 and 3
+ Dafny.DafnyOptions.O.Induction = old == 1 ? 3 : 1;
+ return Dafny.DafnyOptions.O.Induction == 3;
+ }
+
public static bool Verify(Dafny.Program dafnyProgram, ResolverTagger resolver, string uniqueIdPrefix, string requestId, ErrorReporterDelegate er) {
- Dafny.Translator translator = new Dafny.Translator();
+ Dafny.Translator translator = new Dafny.Translator(dafnyProgram.reporter);
translator.InsertChecksums = true;
translator.UniqueIdPrefix = uniqueIdPrefix;
Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index 3dc67098..08040853 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003" ToolsVersion="4.0">
<PropertyGroup>
<MinimumVisualStudioVersion>11.0</MinimumVisualStudioVersion>
@@ -106,7 +106,9 @@
<Reference Include="Houdini">
<HintPath>..\..\..\boogie\Binaries\Houdini.dll</HintPath>
</Reference>
- <Reference Include="Microsoft.VisualStudio.Language.Intellisense, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+ <Reference Include="Microsoft.VisualStudio.Language.Intellisense, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Language.11.0.4\lib\net45\Microsoft.VisualStudio.Language.Intellisense.dll</HintPath>
+ </Reference>
<Reference Include="Model">
<HintPath>..\..\..\boogie\Binaries\Model.dll</HintPath>
</Reference>
@@ -124,23 +126,57 @@
</Reference>
</ItemGroup>
<ItemGroup>
- <Reference Include="Microsoft.VisualStudio.Shell.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.Editor, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.ComponentModelHost, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.Shell.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.Shell.Immutable.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.OLE.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.8.0, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.Shell.Interop.9.0, Version=9.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.CoreUtility, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.TextManager.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
- <Reference Include="Microsoft.VisualStudio.Text.Data, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.Text.Logic, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.Text.UI, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.Text.UI.Wpf, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
- <Reference Include="Microsoft.VisualStudio.Language.StandardClassification, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+ <Reference Include="Microsoft.VisualStudio.Shell.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
+ <HintPath>..\packages\VSSDK.Shell.Interop.7.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Editor, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Editor.11.0.4\lib\net45\Microsoft.VisualStudio.Editor.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.ComponentModelHost, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.ComponentModelHost.11.0.4\lib\net45\Microsoft.VisualStudio.ComponentModelHost.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Shell.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Shell.11.11.0.4\lib\net45\Microsoft.VisualStudio.Shell.11.0.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Shell.Immutable.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Shell.Immutable.10.10.0.4\lib\net40\Microsoft.VisualStudio.Shell.Immutable.10.0.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.OLE.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
+ <HintPath>..\packages\VSSDK.OLE.Interop.7.0.4\lib\net20\Microsoft.VisualStudio.OLE.Interop.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Shell.Interop.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Shell.Interop.11.11.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.11.0.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Shell.Interop.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Shell.Interop.10.10.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.10.0.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Shell.Interop.8.0, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
+ <HintPath>..\packages\VSSDK.Shell.Interop.8.8.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.8.0.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Shell.Interop.9.0, Version=9.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
+ <HintPath>..\packages\VSSDK.Shell.Interop.9.9.0.4\lib\net20\Microsoft.VisualStudio.Shell.Interop.9.0.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.CoreUtility, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.CoreUtility.11.0.4\lib\net45\Microsoft.VisualStudio.CoreUtility.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.TextManager.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
+ <HintPath>..\packages\VSSDK.TextManager.Interop.7.0.4\lib\net20\Microsoft.VisualStudio.TextManager.Interop.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Text.Data, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.Data.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Text.Logic, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.Logic.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Text.UI, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.UI.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Text.UI.Wpf, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Text.11.0.4\lib\net45\Microsoft.VisualStudio.Text.UI.Wpf.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Language.StandardClassification, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <HintPath>..\packages\VSSDK.Language.11.0.4\lib\net45\Microsoft.VisualStudio.Language.StandardClassification.dll</HintPath>
+ </Reference>
</ItemGroup>
<ItemGroup>
<Reference Include="PresentationCore" />
@@ -200,6 +236,9 @@
</Content>
</ItemGroup>
<ItemGroup>
+ <None Include="packages.config">
+ <SubType>Designer</SubType>
+ </None>
<None Include="source.extension.vsixmanifest">
<SubType>Designer</SubType>
</None>
@@ -250,4 +289,4 @@ copy /y "..\Binaries\z3.exe" "$(ProjectDir)"</PreBuildEvent>
<Target Name="AfterBuild">
</Target>
-->
-</Project> \ No newline at end of file
+</Project>
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 3bb8f01c..998a2d7f 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -15,7 +15,6 @@ using Microsoft.VisualStudio.Text.Tagging;
using Microsoft.VisualStudio.Utilities;
using Bpl = Microsoft.Boogie;
-
namespace DafnyLanguage
{
@@ -136,9 +135,8 @@ namespace DafnyLanguage
List<IdRegion> newRegions = new List<IdRegion>();
- foreach (var addInfo in program.AdditionalInformation)
- {
- IdRegion.Add(newRegions, addInfo.Token, addInfo.Text, addInfo.Length);
+ foreach (var info in program.reporter.AllMessages[ErrorLevel.Info]) {
+ IdRegion.Add(newRegions, program, info.token, info.message, info.token.val.Length);
}
foreach (var module in program.Modules) {
@@ -151,73 +149,75 @@ namespace DafnyLanguage
foreach (var ctor in dt.Ctors) {
foreach (var dtor in ctor.Destructors) {
if (dtor.CorrespondingFormal.HasName) {
- IdRegion.Add(newRegions, dtor.tok, dtor, null, "destructor", true, module);
+ IdRegion.Add(newRegions, program, dtor.tok, dtor, null, "destructor", true, module);
}
}
}
} else if (d is IteratorDecl) {
var iter = (IteratorDecl)d;
foreach (var p in iter.Ins) {
- IdRegion.Add(newRegions, p.tok, p, true, module);
+ IdRegion.Add(newRegions, program, p.tok, p, true, module);
}
foreach (var p in iter.Outs) {
- IdRegion.Add(newRegions, p.tok, p, true, "yield-parameter", module);
+ IdRegion.Add(newRegions, program, p.tok, p, true, "yield-parameter", module);
}
- iter.Reads.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));
- iter.Modifies.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));
- iter.Requires.ForEach(e => ExprRegions(e.E, newRegions, module));
- iter.YieldRequires.ForEach(e => ExprRegions(e.E, newRegions, module));
- iter.YieldEnsures.ForEach(e => ExprRegions(e.E, newRegions, module));
- iter.Ensures.ForEach(e => ExprRegions(e.E, newRegions, module));
+ iter.Reads.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module));
+ iter.Modifies.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module));
+ iter.Requires.ForEach(e => ExprRegions(e.E, newRegions, program, module));
+ iter.YieldRequires.ForEach(e => ExprRegions(e.E, newRegions, program, module));
+ iter.YieldEnsures.ForEach(e => ExprRegions(e.E, newRegions, program, module));
+ iter.Ensures.ForEach(e => ExprRegions(e.E, newRegions, program, module));
if (!((ICallable)iter).InferredDecreases) {
- iter.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module));
+ iter.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, program, module));
}
if (iter.Body != null) {
- StatementRegions(iter.Body, newRegions, module);
+ StatementRegions(iter.Body, newRegions, program, module);
}
} else if (d is ClassDecl) {
var cl = (ClassDecl)d;
foreach (var member in cl.Members) {
- if (member is Function) {
+ if (Attributes.Contains(member.Attributes, "auto_generated")) {
+ // do nothing
+ } else if (member is Function) {
var f = (Function)member;
foreach (var p in f.Formals) {
- IdRegion.Add(newRegions, p.tok, p, true, module);
+ IdRegion.Add(newRegions, program, p.tok, p, true, module);
}
- f.Req.ForEach(e => ExprRegions(e, newRegions, module));
- f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));
- f.Ens.ForEach(e => ExprRegions(e, newRegions, module));
- f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module));
+ f.Req.ForEach(e => ExprRegions(e, newRegions, program, module));
+ f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module));
+ f.Ens.ForEach(e => ExprRegions(e, newRegions, program, module));
+ f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, program, module));
if (f.Body != null) {
- ExprRegions(f.Body, newRegions, module);
+ ExprRegions(f.Body, newRegions, program, module);
}
} else if (member is Method) {
var m = (Method)member;
foreach (var p in m.Ins) {
- IdRegion.Add(newRegions, p.tok, p, true, module);
+ IdRegion.Add(newRegions, program, p.tok, p, true, module);
}
foreach (var p in m.Outs) {
- IdRegion.Add(newRegions, p.tok, p, true, module);
+ IdRegion.Add(newRegions, program, p.tok, p, true, module);
}
- m.Req.ForEach(e => ExprRegions(e.E, newRegions, module));
- m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));
- m.Ens.ForEach(e => ExprRegions(e.E, newRegions, module));
- m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module));
+ m.Req.ForEach(e => ExprRegions(e.E, newRegions, program, module));
+ m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, program, module));
+ m.Ens.ForEach(e => ExprRegions(e.E, newRegions, program, module));
+ m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, program, module));
if (m.Body != null) {
- StatementRegions(m.Body, newRegions, module);
+ StatementRegions(m.Body, newRegions, program, module);
}
} else if (member is SpecialField) {
// do nothing
} else if (member is Field) {
var fld = (Field)member;
- IdRegion.Add(newRegions, fld.tok, fld, null, "field", true, module);
+ IdRegion.Add(newRegions, program, fld.tok, fld, null, "field", true, module);
}
}
} else if (d is NewtypeDecl) {
var dd = (NewtypeDecl)d;
if (dd.Var != null) {
- IdRegion.Add(newRegions, dd.Var.tok, dd.Var, true, module);
- ExprRegions(dd.Constraint, newRegions, module);
+ IdRegion.Add(newRegions, program, dd.Var.tok, dd.Var, true, module);
+ ExprRegions(dd.Constraint, newRegions, program, module);
}
}
}
@@ -228,67 +228,80 @@ namespace DafnyLanguage
return true;
}
- static void FrameExprRegions(FrameExpression fe, List<IdRegion> regions, bool descendIntoExpressions, ModuleDefinition module) {
+ static void FrameExprRegions(FrameExpression fe, List<IdRegion> regions, bool descendIntoExpressions, Microsoft.Dafny.Program prog, ModuleDefinition module) {
Contract.Requires(fe != null);
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
if (descendIntoExpressions) {
- ExprRegions(fe.E, regions, module);
+ ExprRegions(fe.E, regions, prog, module);
}
if (fe.Field != null) {
Microsoft.Dafny.Type showType = null; // TODO: if we had the instantiated type of this field, that would have been nice to use here (but the Resolver currently does not compute or store the instantiated type for a FrameExpression)
- IdRegion.Add(regions, fe.tok, fe.Field, showType, "field", false, module);
+ IdRegion.Add(regions, prog, fe.tok, fe.Field, showType, "field", false, module);
}
}
- static void ExprRegions(Microsoft.Dafny.Expression expr, List<IdRegion> regions, ModuleDefinition module) {
+ static void ExprRegions(Microsoft.Dafny.Expression expr, List<IdRegion> regions, Microsoft.Dafny.Program prog, ModuleDefinition module) {
Contract.Requires(expr != null);
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
if (expr is AutoGeneratedExpression) {
// do nothing
return;
} else if (expr is IdentifierExpr) {
var e = (IdentifierExpr)expr;
- IdRegion.Add(regions, e.tok, e.Var, false, module);
+ IdRegion.Add(regions, prog, e.tok, e.Var, false, module);
} else if (expr is MemberSelectExpr) {
var e = (MemberSelectExpr)expr;
var field = e.Member as Field;
if (field != null) {
- IdRegion.Add(regions, e.tok, field, e.Type, "field", false, module);
+ IdRegion.Add(regions, prog, e.tok, field, e.Type, "field", false, module);
}
} else if (expr is LetExpr) {
var e = (LetExpr)expr;
foreach (var bv in e.BoundVars) {
- IdRegion.Add(regions, bv.tok, bv, true, module);
+ IdRegion.Add(regions, prog, bv.tok, bv, true, module);
}
} else if (expr is ComprehensionExpr) {
var e = (ComprehensionExpr)expr;
foreach (var bv in e.BoundVars) {
- IdRegion.Add(regions, bv.tok, bv, true, module);
+ IdRegion.Add(regions, prog, bv.tok, bv, true, module);
}
} else if (expr is MatchExpr) {
var e = (MatchExpr)expr;
foreach (var kase in e.Cases) {
- kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
+ kase.Arguments.ForEach(bv => {
+ IdRegion.Add(regions, prog, bv.tok, bv, true, module);
+ // if the arguments is an encapsulation of different boundvars from nested match cases,
+ // add the boundvars so that they can show up in the IDE correctly
+ if (bv.tok is MatchCaseToken) {
+ MatchCaseToken mt = (MatchCaseToken)bv.tok;
+ foreach(Tuple<Bpl.IToken, BoundVar, bool> entry in mt.varList) {
+ IdRegion.Add(regions, prog, entry.Item1, entry.Item2, entry.Item3, module);
+ }
+ }
+ });
}
} else if (expr is ChainingExpression) {
var e = (ChainingExpression)expr;
// Do the subexpressions only once (that is, avoid the duplication that occurs in the desugared form of the ChainingExpression)
- e.Operands.ForEach(ee => ExprRegions(ee, regions, module));
+ e.Operands.ForEach(ee => ExprRegions(ee, regions, prog, module));
return; // return here, so as to avoid doing the subexpressions below
}
foreach (var ee in expr.SubExpressions) {
- ExprRegions(ee, regions, module);
+ ExprRegions(ee, regions, prog, module);
}
}
- static void StatementRegions(Statement stmt, List<IdRegion> regions, ModuleDefinition module) {
+ static void StatementRegions(Statement stmt, List<IdRegion> regions, Microsoft.Dafny.Program prog, ModuleDefinition module) {
Contract.Requires(stmt != null);
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
if (stmt is VarDeclStmt) {
var s = (VarDeclStmt)stmt;
// Add the variables here, once, and then go directly to the RHS's (without letting the sub-statements re-do the LHS's)
foreach (var local in s.Locals) {
- IdRegion.Add(regions, local.Tok, local, true, module);
+ IdRegion.Add(regions, prog, local.Tok, local, true, module);
}
if (s.Update == null) {
// the VarDeclStmt has no associated assignment
@@ -296,48 +309,58 @@ namespace DafnyLanguage
var upd = (UpdateStmt)s.Update;
foreach (var rhs in upd.Rhss) {
foreach (var ee in rhs.SubExpressions) {
- ExprRegions(ee, regions, module);
+ ExprRegions(ee, regions, prog, module);
}
}
} else {
var upd = (AssignSuchThatStmt)s.Update;
- ExprRegions(upd.Expr, regions, module);
+ ExprRegions(upd.Expr, regions, prog, module);
}
// we're done, so don't do the sub-statements/expressions again
return;
} else if (stmt is ForallStmt) {
var s = (ForallStmt)stmt;
- s.BoundVars.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
+ s.BoundVars.ForEach(bv => IdRegion.Add(regions, prog, bv.tok, bv, true, module));
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
foreach (var kase in s.Cases) {
- kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
+ kase.Arguments.ForEach(bv => {
+ IdRegion.Add(regions, prog, bv.tok, bv, true, module);
+ // if the arguments is an encapsulation of different boundvars from nested match cases,
+ // add the boundvars so that they can show up in the IDE correctly
+ if (bv.tok is MatchCaseToken) {
+ MatchCaseToken mt = (MatchCaseToken)bv.tok;
+ foreach (Tuple<Bpl.IToken, BoundVar, bool> entry in mt.varList) {
+ IdRegion.Add(regions, prog, entry.Item1, entry.Item2, entry.Item3, module);
+ }
+ }
+ });
}
} else if (stmt is LoopStmt) {
var s = (LoopStmt)stmt;
if (s.Mod.Expressions != null) {
- s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false, module));
+ s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false, prog, module));
}
} else if (stmt is CalcStmt) {
var s = (CalcStmt)stmt;
// skip the last line, which is just a duplicate anyway
for (int i = 0; i < s.Lines.Count - 1; i++) {
- ExprRegions(s.Lines[i], regions, module);
+ ExprRegions(s.Lines[i], regions, prog, module);
}
foreach (var ss in stmt.SubStatements) {
- StatementRegions(ss, regions, module);
+ StatementRegions(ss, regions, prog, module);
}
return;
}
foreach (var ee in stmt.SubExpressions) {
- ExprRegions(ee, regions, module);
+ ExprRegions(ee, regions, prog, module);
}
foreach (var ss in stmt.SubStatements) {
- StatementRegions(ss, regions, module);
+ StatementRegions(ss, regions, prog, module);
}
}
- class IdRegion
+ class IdRegion : DafnyRegion
{
public readonly int Start;
public readonly int Length;
@@ -346,40 +369,39 @@ namespace DafnyLanguage
public readonly OccurrenceKind Kind;
public readonly IVariable Variable;
- static bool SurfaceSyntaxToken(Bpl.IToken tok) {
- Contract.Requires(tok != null);
- return !(tok is TokenWrapper);
- }
-
- public static void Add(List<IdRegion> regions, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) {
+ public static void Add(List<IdRegion> regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) {
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
Contract.Requires(tok != null);
Contract.Requires(v != null);
- Add(regions, tok, v, isDefinition, null, context);
+ Add(regions, prog, tok, v, isDefinition, null, context);
}
- public static void Add(List<IdRegion> regions, Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) {
+ public static void Add(List<IdRegion> regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) {
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
Contract.Requires(tok != null);
Contract.Requires(v != null);
- if (SurfaceSyntaxToken(tok)) {
+ if (InMainFileAndUserDefined(prog, tok)) {
regions.Add(new IdRegion(tok, v, isDefinition, kind, context));
}
}
- public static void Add(List<IdRegion> regions, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {
+ public static void Add(List<IdRegion> regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
Contract.Requires(tok != null);
Contract.Requires(decl != null);
Contract.Requires(kind != null);
- if (SurfaceSyntaxToken(tok)) {
+ if (InMainFileAndUserDefined(prog, tok)) {
regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context));
}
}
- public static void Add(List<IdRegion> regions, Bpl.IToken tok, string text, int length) {
+ public static void Add(List<IdRegion> regions, Microsoft.Dafny.Program prog, Bpl.IToken tok, string text, int length) {
Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
Contract.Requires(tok != null);
Contract.Requires(text != null);
- if (SurfaceSyntaxToken(tok)) {
+ if (InMainFileAndUserDefined(prog, tok)) {
regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length));
}
}
@@ -433,6 +455,15 @@ namespace DafnyLanguage
}
}
+ public abstract class DafnyRegion
+ {
+ public static bool InMainFileAndUserDefined(Microsoft.Dafny.Program prog, Bpl.IToken tok) {
+ Contract.Requires(prog != null);
+ Contract.Requires(tok != null);
+ return object.Equals(prog.FullName, tok.filename) && !(tok is AutoGeneratedToken);
+ }
+ }
+
#endregion
}
diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs
index 11e1287f..0e061cd3 100644
--- a/Source/DafnyExtension/MenuProxy.cs
+++ b/Source/DafnyExtension/MenuProxy.cs
@@ -33,6 +33,14 @@ namespace DafnyLanguage
&& 0 < DafnyDriver.IncrementalVerificationMode();
}
+ public bool ToggleAutomaticInduction(IWpfTextView activeTextView) {
+ return DafnyDriver.ChangeAutomaticInduction();
+ }
+
+ public bool AutomaticInductionCommandEnabled(IWpfTextView activeTextView) {
+ return activeTextView != null;
+ }
+
public bool StopVerifierCommandEnabled(IWpfTextView activeTextView)
{
DafnyLanguage.ProgressTagger tagger;
@@ -67,6 +75,15 @@ namespace DafnyLanguage
}
}
+ public void DiagnoseTimeouts(IWpfTextView activeTextView)
+ {
+ DafnyLanguage.ProgressTagger tagger;
+ if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger))
+ {
+ tagger.StartVerification(false, true);
+ }
+ }
+
public bool MenuEnabled(IWpfTextView activeTextView)
{
return activeTextView != null && activeTextView.TextBuffer.ContentType.DisplayName == "dafny";
@@ -80,6 +97,14 @@ namespace DafnyLanguage
&& resolver.Program != null;
}
+ public bool DiagnoseTimeoutsCommandEnabled(IWpfTextView activeTextView)
+ {
+ ResolverTagger resolver;
+ return activeTextView != null
+ && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
+ && resolver.VerificationErrors.Any(err => err.Message.Contains("timed out"));
+ }
+
public void Compile(IWpfTextView activeTextView)
{
ResolverTagger resolver;
diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs
index 85771e94..fc06d4bf 100644
--- a/Source/DafnyExtension/OutliningTagger.cs
+++ b/Source/DafnyExtension/OutliningTagger.cs
@@ -80,7 +80,7 @@ namespace DafnyLanguage
if (start == end) yield break;
foreach (var r in _regions) {
- if (0 <= r.Length && r.Start >= start && r.Start + r.Length <= end) {
+ if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) {
yield return new TagSpan<OutliningRegionTag>(
new SnapshotSpan(_snapshot, r.Start, r.Length),
new OutliningRegionTag(false, false, "...", r.HoverText));
@@ -130,18 +130,18 @@ namespace DafnyLanguage
if (module.IsAbstract) {
nm = "abstract " + nm;
}
- newRegions.Add(new OutliningRegion(module, nm));
+ OutliningRegion.Add(newRegions, program, module, nm);
}
foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) {
if (!HasBodyTokens(d) && !(d is Dafny.ClassDecl)) {
continue;
}
if (d is Dafny.OpaqueTypeDecl) {
- newRegions.Add(new OutliningRegion(d, "type"));
+ OutliningRegion.Add(newRegions, program, d, "type");
} else if (d is Dafny.CoDatatypeDecl) {
- newRegions.Add(new OutliningRegion(d, "codatatype"));
+ OutliningRegion.Add(newRegions, program, d, "codatatype");
} else if (d is Dafny.DatatypeDecl) {
- newRegions.Add(new OutliningRegion(d, "datatype"));
+ OutliningRegion.Add(newRegions, program, d, "datatype");
} else if (d is Dafny.ModuleDecl) {
// do nothing here, since the outer loop handles modules
} else {
@@ -149,9 +149,9 @@ namespace DafnyLanguage
if (cl.IsDefaultClass) {
// do nothing
} else if (cl is Dafny.IteratorDecl) {
- newRegions.Add(new OutliningRegion(cl, "iterator"));
+ OutliningRegion.Add(newRegions, program, cl, "iterator");
} else {
- newRegions.Add(new OutliningRegion(cl, "class"));
+ OutliningRegion.Add(newRegions, program, cl, "class");
}
// do the class members (in particular, functions and methods)
foreach (Dafny.MemberDecl m in cl.Members) {
@@ -168,7 +168,7 @@ namespace DafnyLanguage
if (!m.IsGhost) {
nm += " method";
}
- newRegions.Add(new OutliningRegion(m, nm));
+ OutliningRegion.Add(newRegions, program, m, nm);
} else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) {
var nm =
m is Dafny.Constructor ? "constructor" :
@@ -179,7 +179,7 @@ namespace DafnyLanguage
if (m.IsGhost && !(m is Dafny.CoLemma)) {
nm = "ghost " + nm;
}
- newRegions.Add(new OutliningRegion(m, nm));
+ OutliningRegion.Add(newRegions, program, m, nm);
}
}
}
@@ -196,12 +196,20 @@ namespace DafnyLanguage
return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken;
}
- class OutliningRegion
+ class OutliningRegion : DafnyRegion
{
+ public static void Add(List<OutliningRegion> regions, Microsoft.Dafny.Program prog, Dafny.INamedRegion decl, string kind) {
+ Contract.Requires(regions != null);
+ Contract.Requires(prog != null);
+ if (InMainFileAndUserDefined(prog, decl.BodyStartTok)) {
+ regions.Add(new OutliningRegion(decl, kind));
+ }
+ }
+
public readonly int Start;
public readonly int Length;
public readonly string HoverText;
- public OutliningRegion(Dafny.INamedRegion decl, string kind) {
+ private OutliningRegion(Dafny.INamedRegion decl, string kind) {
int startPosition = decl.BodyStartTok.pos + 1; // skip the open-curly brace itself
int length = decl.BodyEndTok.pos - startPosition;
Start = startPosition;
diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index b4e58d3d..c3f56259 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -197,6 +197,7 @@ namespace DafnyLanguage
bool verificationInProgress; // this field is protected by "this". Invariant: !verificationInProgress ==> bufferChangesPreVerificationStart.Count == 0
System.Threading.Tasks.Task verificationTask;
public bool VerificationDisabled { get; private set; }
+ bool isDiagnosingTimeouts;
string lastRequestId;
public static readonly IDictionary<ITextBuffer, ProgressTagger> ProgressTaggers = new ConcurrentDictionary<ITextBuffer, ProgressTagger>();
@@ -227,14 +228,21 @@ namespace DafnyLanguage
if (prog == null || VerificationDisabled) return;
// We have a successfully resolved program to verify
- var resolvedVersion = snap.Version.VersionNumber;
- if (bufferChangesPostVerificationStart.Count == 0) {
- // Nothing new to verify. No reason to start a new verification.
- return;
- } else if (!bufferChangesPostVerificationStart.TrueForAll(span => span.Snapshot.Version.VersionNumber <= resolvedVersion)) {
- // There have been buffer changes since the program that was resolved. Do nothing here,
- // and instead just await the next resolved program.
- return;
+ var dt = isDiagnosingTimeouts;
+ if (!dt)
+ {
+ var resolvedVersion = snap.Version.VersionNumber;
+ if (bufferChangesPostVerificationStart.Count == 0)
+ {
+ // Nothing new to verify. No reason to start a new verification.
+ return;
+ }
+ else if (!bufferChangesPostVerificationStart.TrueForAll(span => span.Snapshot.Version.VersionNumber <= resolvedVersion))
+ {
+ // There have been buffer changes since the program that was resolved. Do nothing here,
+ // and instead just await the next resolved program.
+ return;
+ }
}
// at this time, we're committed to running the verifier
@@ -254,10 +262,14 @@ namespace DafnyLanguage
}
verificationTask = System.Threading.Tasks.Task.Factory.StartNew(
- () => RunVerifier(prog, snap, lastRequestId, resolver),
+ () => RunVerifier(prog, snap, lastRequestId, resolver, dt),
TaskCreationOptions.LongRunning);
verificationInProgress = true;
+ if (dt)
+ {
+ isDiagnosingTimeouts = false;
+ }
// Change orange progress markers into yellow ones
Contract.Assert(bufferChangesPreVerificationStart.Count == 0); // follows from monitor invariant
@@ -293,7 +305,7 @@ namespace DafnyLanguage
}
}
- public void StartVerification()
+ public void StartVerification(bool clearCache = true, bool diagnoseTimeouts = false)
{
lock (this)
{
@@ -301,7 +313,11 @@ namespace DafnyLanguage
bufferChangesPostVerificationStart.Clear();
bufferChangesPostVerificationStart.Add(new SnapshotSpan(_buffer.CurrentSnapshot, 0, _buffer.CurrentSnapshot.Length));
VerificationDisabled = false;
- ClearCachedVerificationResults();
+ isDiagnosingTimeouts = diagnoseTimeouts;
+ if (clearCache)
+ {
+ ClearCachedVerificationResults();
+ }
NotifyAboutChangedTags(_buffer.CurrentSnapshot);
}
}
@@ -314,7 +330,7 @@ namespace DafnyLanguage
}
}
- void RunVerifier(Dafny.Program program, ITextSnapshot snapshot, string requestId, ResolverTagger errorListHolder) {
+ void RunVerifier(Dafny.Program program, ITextSnapshot snapshot, string requestId, ResolverTagger errorListHolder, bool diagnoseTimeouts) {
Contract.Requires(program != null);
Contract.Requires(snapshot != null);
Contract.Requires(requestId != null);
@@ -332,6 +348,8 @@ namespace DafnyLanguage
_version++;
}
+ DafnyDriver.SetDiagnoseTimeouts(diagnoseTimeouts);
+
try
{
bool success = DafnyDriver.Verify(program, errorListHolder, GetHashCode().ToString(), requestId, errorInfo =>
@@ -369,6 +387,10 @@ namespace DafnyLanguage
{
errorListHolder.AddError(new DafnyError("$$program$$", 0, 0, ErrorCategory.InternalError, "Verification process error: " + e.Message, snapshot, false), "$$program$$", requestId);
}
+ finally
+ {
+ DafnyDriver.SetDiagnoseTimeouts(!diagnoseTimeouts);
+ }
lock (this) {
bufferChangesPreVerificationStart.Clear();
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 1fdd3827..4a50a4e8 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -68,26 +68,27 @@ namespace DafnyLanguage
{
Error = error;
}
-
- private static string ConvertToErrorType(DafnyError err)
- {
- string ty; // the COLORs below indicate what I see on my machine
- switch (err.Category)
- {
- default: // unexpected category
+
+ private static string ConvertToErrorType(DafnyError err) {
+ // the COLORs below indicate what I see on my machine
+ switch (err.Category) {
+ case ErrorCategory.ProcessError:
case ErrorCategory.ParseError:
- case ErrorCategory.ParseWarning:
- ty = "syntax error"; break; // COLOR: red
+ return "syntax error"; // COLOR: red
case ErrorCategory.ResolveError:
- ty = "compiler error"; break; // COLOR: blue
+ return "compiler error"; // COLOR: blue
+ case ErrorCategory.ParseWarning:
+ case ErrorCategory.ResolveWarning:
+ return "compiler warning"; // COLOR: blue
+ case ErrorCategory.InternalError:
case ErrorCategory.VerificationError:
- ty = "error"; break; // COLOR: red
+ return "error"; // COLOR: red
case ErrorCategory.AuxInformation:
- ty = "other error"; break; // COLOR: purple red
- case ErrorCategory.InternalError:
- ty = "error"; break; // COLOR: red
+ return "other error"; // COLOR: purple red
+ default:
+ Contract.Assert(false);
+ throw new InvalidOperationException();
}
- return ty;
}
}
@@ -188,7 +189,7 @@ namespace DafnyLanguage
{
get
{
- return _verificationErrors.Values.Where(ec => ec.RequestId == MostRecentRequestId).SelectMany(ec => ec.Errors.Reverse());
+ return _verificationErrors.Values.Where(ec => ec.RequestId == MostRecentRequestId).SelectMany(ec => ec.Errors.Reverse()).ToList();
}
}
@@ -198,13 +199,19 @@ namespace DafnyLanguage
{
lock (this)
{
- if (_resolutionErrors != null && _resolutionErrors.Any())
- {
- return _resolutionErrors;
+ bool anyResolutionErrors = false;
+ if (_resolutionErrors != null) {
+ foreach (var err in _resolutionErrors) {
+ if (CategoryConversion(err.Category) == TaskErrorCategory.Error) {
+ anyResolutionErrors = true;
+ }
+ yield return err;
+ }
}
- else
- {
- return VerificationErrors;
+ if (!anyResolutionErrors) {
+ foreach (var err in VerificationErrors) {
+ yield return err;
+ }
}
}
}
@@ -310,19 +317,18 @@ namespace DafnyLanguage
/// <summary>
/// Calls the Dafny parser/resolver/type checker on the contents of the buffer, updates the Error List accordingly.
/// </summary>
- void ResolveBuffer(object sender, EventArgs args)
- {
+ void ResolveBuffer(object sender, EventArgs args) {
ITextSnapshot snapshot = _buffer.CurrentSnapshot;
if (snapshot == Snapshot)
return; // we've already done this snapshot
string filename = _document != null ? _document.FilePath : "<program>";
- var driver = new DafnyDriver(snapshot, filename);
+ var driver = new DafnyDriver(_buffer, filename);
List<DafnyError> newErrors;
Dafny.Program program;
try
{
- program = driver.ProcessResolution();
+ program = driver.ProcessResolution(true);
newErrors = driver.Errors;
}
catch (Exception e)
@@ -353,49 +359,46 @@ namespace DafnyLanguage
public void UpdateErrorList(ITextSnapshot snapshot)
{
- lock (this)
+ if (_errorProvider != null && !m_disposed)
{
- if (_errorProvider != null && !m_disposed)
- {
- _errorProvider.SuspendRefresh(); // reduce flickering
- _errorProvider.Tasks.Clear();
- foreach (var err in AllErrors)
- {
- var lineNum = 0;
- var columnNum = 0;
- if (err.Span != null) {
- var span = err.Span.GetSpan(snapshot);
- lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position);
- var line = snapshot.GetLineFromPosition(span.Start.Position);
- columnNum = span.Start - line.Start;
- } else {
- lineNum = err.Line;
- columnNum = err.Column;
- }
-
- ErrorTask task = new ErrorTask()
- {
- Category = TaskCategory.BuildCompile,
- ErrorCategory = CategoryConversion(err.Category),
- Text = err.Message,
- Line = lineNum,
- Column = columnNum
- };
- if (err.Filename != null) {
- task.Document = err.Filename;
- }
- else if (_document != null)
- {
- task.Document = _document.FilePath;
- }
- if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError)
- {
- task.Navigate += new EventHandler(NavigateHandler);
- }
- _errorProvider.Tasks.Add(task);
+ _errorProvider.SuspendRefresh(); // reduce flickering
+ _errorProvider.Tasks.Clear();
+ foreach (var err in AllErrors)
+ {
+ var lineNum = 0;
+ var columnNum = 0;
+ if (err.Span != null) {
+ var span = err.Span.GetSpan(snapshot);
+ lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position);
+ var line = snapshot.GetLineFromPosition(span.Start.Position);
+ columnNum = span.Start - line.Start;
+ } else {
+ lineNum = err.Line;
+ columnNum = err.Column;
+ }
+
+ ErrorTask task = new ErrorTask()
+ {
+ Category = TaskCategory.BuildCompile,
+ ErrorCategory = CategoryConversion(err.Category),
+ Text = err.Message,
+ Line = lineNum,
+ Column = columnNum
+ };
+ if (err.Filename != null) {
+ task.Document = err.Filename;
+ }
+ else if (_document != null)
+ {
+ task.Document = _document.FilePath;
+ }
+ if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError)
+ {
+ task.Navigate += new EventHandler(NavigateHandler);
}
- _errorProvider.ResumeRefresh();
+ _errorProvider.Tasks.Add(task);
}
+ _errorProvider.ResumeRefresh();
}
var chng = TagsChanged;
if (chng != null)
@@ -412,6 +415,7 @@ namespace DafnyLanguage
case ErrorCategory.InternalError:
return TaskErrorCategory.Error;
case ErrorCategory.ParseWarning:
+ case ErrorCategory.ResolveWarning:
return TaskErrorCategory.Warning;
case ErrorCategory.AuxInformation:
return TaskErrorCategory.Message;
@@ -477,7 +481,7 @@ namespace DafnyLanguage
public enum ErrorCategory
{
- ProcessError, ParseWarning, ParseError, ResolveError, VerificationError, AuxInformation, InternalError
+ ProcessError, ParseWarning, ParseError, ResolveWarning, ResolveError, VerificationError, AuxInformation, InternalError
}
public class DafnyError
@@ -527,7 +531,7 @@ namespace DafnyLanguage
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 column = Math.Max(0, int.Parse(match.Groups[2].Value));
var sLine = Snapshot.GetLineFromLineNumber(line);
Contract.Assert(column <= sLine.Length);
var sLength = Math.Max(0, Math.Min(sLine.Length - column, 0));
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index af141ad7..7a5eb572 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -70,17 +70,34 @@ namespace DafnyLanguage
}
}
+
internal sealed class DafnyTokenTagger : ITagger<DafnyTokenTag>, IDisposable
{
+ internal sealed class ScanResult
+ {
+ internal ITextSnapshot _oldSnapshot;
+ internal ITextSnapshot _newSnapshot;
+ internal List<TokenRegion> _regions; // the regions computed for the _newSnapshot
+ internal NormalizedSnapshotSpanCollection _difference; // the difference between _oldSnapshot and _newSnapshot
+
+ internal ScanResult(ITextSnapshot oldSnapshot, ITextSnapshot newSnapshot, List<TokenRegion> regions, NormalizedSnapshotSpanCollection diffs) {
+ _oldSnapshot = oldSnapshot;
+ _newSnapshot = newSnapshot;
+ _regions = regions;
+ _difference = diffs;
+ }
+ }
+
ITextBuffer _buffer;
ITextSnapshot _snapshot;
List<TokenRegion> _regions;
+ static object bufferTokenTaggerKey = new object();
bool _disposed;
internal DafnyTokenTagger(ITextBuffer buffer) {
_buffer = buffer;
_snapshot = buffer.CurrentSnapshot;
- _regions = Rescan(_snapshot);
+ _regions = Scan(_snapshot);
_buffer.Changed += new EventHandler<TextContentChangedEventArgs>(ReparseFile);
}
@@ -89,6 +106,7 @@ namespace DafnyLanguage
lock (this) {
if (!_disposed) {
_buffer.Changed -= ReparseFile;
+ _buffer.Properties.RemoveProperty(bufferTokenTaggerKey);
_buffer = null;
_snapshot = null;
_regions = null;
@@ -127,24 +145,93 @@ namespace DafnyLanguage
ITextSnapshot snapshot = _buffer.CurrentSnapshot;
if (snapshot == _snapshot)
return; // we've already computed the regions for this snapshot
+
+ NormalizedSnapshotSpanCollection difference = new NormalizedSnapshotSpanCollection();
+ ScanResult result;
+ if (_buffer.Properties.TryGetProperty(bufferTokenTaggerKey, out result) &&
+ (result._oldSnapshot == _snapshot) &&
+ (result._newSnapshot == snapshot)) {
+ difference = result._difference;
+ // save the new baseline
+ _regions = result._regions;
+ _snapshot = snapshot;
+ } else {
+ List<TokenRegion> regions = new List<TokenRegion>();
+ List<SnapshotSpan> rescannedRegions = new List<SnapshotSpan>();
+
+ // loop through the changes and check for changes in comments first. If
+ // the change is in a comments, we need to rescan starting from the
+ // beginning of the comments (which in multi-lined comments, it can
+ // be a line that the changes are not on), otherwise, we can just rescan the lines
+ // that the changes are on.
+ bool done;
+ SnapshotPoint start, end;
+ for (int i = 0; i < args.Changes.Count; i++) {
+ done = false;
+ // get the span of the lines that the change is on.
+ int cStart = args.Changes[i].NewSpan.Start;
+ int cEnd = args.Changes[i].NewSpan.End;
+ start = snapshot.GetLineFromPosition(cStart).Start;
+ end = snapshot.GetLineFromPosition(cEnd).End;
+ SnapshotSpan newSpan = new SnapshotSpan(start, end);
+ foreach (TokenRegion r in _regions) {
+ if (r.Kind == DafnyTokenKind.Comment) {
+ // if the change is in the comments, we want to start scanning from the
+ // the beginning of the comments instead.
+ SnapshotSpan span = r.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive);
+ if (span.IntersectsWith(newSpan)) {
+ start = span.Start.Position < newSpan.Start.Position ? span.Start : newSpan.Start;
+ end = span.End.Position > newSpan.End.Position ? span.End : newSpan.End;
+ end = Scan(snapshot.GetText(new SnapshotSpan(start, end)), start, regions, snapshot);
+ // record the regions that we rescanned.
+ rescannedRegions.Add(new SnapshotSpan(start, end));
+ done = true;
+ break;
+ }
+ }
+ }
+ if (!done) {
+ // scan the lines that the change is on to generate the new regions.
+ end = Scan(snapshot.GetText(new SnapshotSpan(start, end)), start, regions, snapshot);
+ // record the span that we rescanned.
+ rescannedRegions.Add(new SnapshotSpan(start, end));
+ }
+ }
- // get all of the outline regions in the snapshot
- List<TokenRegion> newRegions = Rescan(snapshot);
-
- // determine the changed span, and send a changed event with the new spans
- List<SnapshotSpan> oldSpans = new List<SnapshotSpan>(_regions.Select(r =>
- r.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive)));
-
- List<SnapshotSpan> newSpans = new List<SnapshotSpan>(newRegions.Select(r => r.Span));
-
- NormalizedSnapshotSpanCollection oldSpanCollection = new NormalizedSnapshotSpanCollection(oldSpans);
- NormalizedSnapshotSpanCollection newSpanCollection = new NormalizedSnapshotSpanCollection(newSpans);
-
- NormalizedSnapshotSpanCollection difference = SymmetricDifference(oldSpanCollection, newSpanCollection);
-
- // save the new baseline
- _snapshot = snapshot;
- _regions = newRegions;
+ List<SnapshotSpan> oldSpans = new List<SnapshotSpan>();
+ List<SnapshotSpan> newSpans = new List<SnapshotSpan>();
+ // record the newly created spans.
+ foreach (TokenRegion r in regions) {
+ newSpans.Add(r.Span);
+ }
+ // loop through the old scan results and remove the ones that
+ // are in the regions that are rescanned.
+ foreach (TokenRegion r in _regions) {
+ SnapshotSpan origSpan = r.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive);
+ bool obsolete = false;
+ foreach (SnapshotSpan span in rescannedRegions) {
+ if (origSpan.IntersectsWith(span)) {
+ oldSpans.Add(span);
+ obsolete = true;
+ break;
+ }
+ }
+ if (!obsolete) {
+ TokenRegion region = new TokenRegion(origSpan.Start, origSpan.End, r.Kind);
+ regions.Add(region);
+ }
+ }
+
+ NormalizedSnapshotSpanCollection oldSpanCollection = new NormalizedSnapshotSpanCollection(oldSpans);
+ NormalizedSnapshotSpanCollection newSpanCollection = new NormalizedSnapshotSpanCollection(newSpans);
+ difference = SymmetricDifference(oldSpanCollection, newSpanCollection);
+
+ // save the scan result
+ _buffer.Properties[bufferTokenTaggerKey] = new ScanResult(_snapshot, snapshot, regions, difference);
+ // save the new baseline
+ _snapshot = snapshot;
+ _regions = regions;
+ }
var chng = TagsChanged;
if (chng != null) {
@@ -160,38 +247,35 @@ namespace DafnyLanguage
NormalizedSnapshotSpanCollection.Difference(second, first));
}
- private static List<TokenRegion> Rescan(ITextSnapshot newSnapshot) {
- List<TokenRegion> newRegions = new List<TokenRegion>();
-
+ private static SnapshotPoint Scan(string txt, SnapshotPoint start, List<TokenRegion> newRegions, ITextSnapshot newSnapshot) {
int longCommentDepth = 0;
- SnapshotPoint commentStart = new SnapshotPoint(); // used only when longCommentDepth != 0
+ SnapshotPoint commentStart = new SnapshotPoint();
SnapshotPoint commentEndAsWeKnowIt = new SnapshotPoint(); // used only when longCommentDepth != 0
- foreach (ITextSnapshotLine line in newSnapshot.Lines) {
- string txt = line.GetText(); // the current line (without linebreak characters)
- int N = txt.Length; // length of the current line
- int cur = 0; // offset into the current line
-
+ int N = txt.Length;
+ bool done = false;
+ while (!done) {
+ N = txt.Length; // length of the current buffer
+ int cur = 0; // offset into the current buffer
if (longCommentDepth != 0) {
ScanForEndOfComment(txt, ref longCommentDepth, ref cur);
if (longCommentDepth == 0) {
// we just finished parsing a long comment
- newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + cur), DafnyTokenKind.Comment));
+ newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, start + cur), DafnyTokenKind.Comment));
} else {
// we're still parsing the long comment
Contract.Assert(cur == txt.Length);
- commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + cur);
+ commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, start + cur);
goto OUTER_CONTINUE;
}
}
-
- // repeatedly get the remaining tokens from this line
- int end; // offset into the current line
+ // repeatedly get the remaining tokens from this buffer
+ int end; // offset into the current buffer
for (; ; cur = end) {
// advance to the first character of a keyword or token
DafnyTokenKind ty = DafnyTokenKind.Keyword;
for (; ; cur++) {
if (N <= cur) {
- // we've looked at everything in this line
+ // we've looked at everything in this buffer
goto OUTER_CONTINUE;
}
char ch = txt[cur];
@@ -204,7 +288,7 @@ namespace DafnyLanguage
}
// advance to the end of the token
- end = cur + 1; // offset into the current line
+ end = cur + 1; // offset into the current buffer
if (ty == DafnyTokenKind.Number) {
// scan the rest of this number
for (; end < N; end++) {
@@ -213,7 +297,7 @@ namespace DafnyLanguage
} else break;
}
} else if (ty == DafnyTokenKind.String) {
- // scan the rest of this string, but not past the end-of-line
+ // scan the rest of this string, but not past the end-of-buffer
for (; end < N; end++) {
char ch = txt[end];
if (ch == '"') {
@@ -233,20 +317,20 @@ namespace DafnyLanguage
if (end == N) continue; // this was not the start of a comment; it was just a single "/" and we don't care to color it
char ch = txt[end];
if (ch == '/') {
- // a short comment
- end = N;
+ // a short comment, to the end of the line.
+ end = newSnapshot.GetLineFromPosition(start + end).End.Position - start;
} else if (ch == '*') {
// a long comment; find the matching "*/"
end++;
- commentStart = new SnapshotPoint(newSnapshot, line.Start + cur);
+ commentStart = new SnapshotPoint(newSnapshot, start + cur);
Contract.Assert(longCommentDepth == 0);
longCommentDepth = 1;
ScanForEndOfComment(txt, ref longCommentDepth, ref end);
if (longCommentDepth == 0) {
// we finished scanning a long comment, and "end" is set to right after it
- newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + end), DafnyTokenKind.Comment));
+ newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, start + end), DafnyTokenKind.Comment));
} else {
- commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + end);
+ commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, start + end);
}
continue;
} else {
@@ -305,6 +389,7 @@ namespace DafnyLanguage
case "ghost":
case "if":
case "imap":
+ case "iset":
case "import":
case "in":
case "include":
@@ -357,21 +442,54 @@ namespace DafnyLanguage
}
}
}
-
- newRegions.Add(new TokenRegion(new SnapshotPoint(newSnapshot, line.Start + cur), new SnapshotPoint(newSnapshot, line.Start + end), ty));
+ newRegions.Add(new TokenRegion(new SnapshotPoint(newSnapshot, start + cur), new SnapshotPoint(newSnapshot, start + end), ty));
+ }
+ OUTER_CONTINUE:
+ done = true;
+ if (longCommentDepth != 0) {
+ // we need to look into the next line
+ ITextSnapshotLine currLine = newSnapshot.GetLineFromPosition(start + N);
+ if ((currLine.LineNumber + 1) < newSnapshot.LineCount) {
+ ITextSnapshotLine nextLine = newSnapshot.GetLineFromLineNumber(currLine.LineNumber + 1);
+ txt = nextLine.GetText();
+ start = nextLine.Start;
+ // we are done scanning the current buffer, but not the whole file yet.
+ // we need to continue to find the enclosing "*/", or until the end of the file.
+ done = false;
+ } else {
+ // This was a malformed comment, running to the end of the buffer. Above, we let "commentEndAsWeKnowIt" be the end of the
+ // last line, so we can use it here.
+ newRegions.Add(new TokenRegion(commentStart, commentEndAsWeKnowIt, DafnyTokenKind.Comment));
+ }
}
- OUTER_CONTINUE: ;
}
+ return new SnapshotPoint(newSnapshot, start + N);
+ }
- if (longCommentDepth != 0) {
- // This was a malformed comment, running to the end of the buffer. Above, we let "commentEndAsWeKnowIt" be the end of the
- // last line, so we can use it here.
- newRegions.Add(new TokenRegion(commentStart, commentEndAsWeKnowIt, DafnyTokenKind.Comment));
+ private List<TokenRegion> Scan(ITextSnapshot newSnapshot) {
+ List<TokenRegion> newRegions;
+ ScanResult result;
+ if (_buffer.Properties.TryGetProperty(bufferTokenTaggerKey, out result) &&
+ result._newSnapshot == newSnapshot) {
+ newRegions = result._regions;
+ } else {
+ newRegions = new List<TokenRegion>();
+ int nextLineNumber = -1;
+ foreach (ITextSnapshotLine line in newSnapshot.Lines) {
+ if (line.LineNumber <= nextLineNumber) {
+ // the line is already processed.
+ continue;
+ }
+ string txt = line.GetText(); // the current line (without linebreak characters)
+ SnapshotPoint end = Scan(txt, line.Start, newRegions, newSnapshot);
+ nextLineNumber = newSnapshot.GetLineFromPosition(end).LineNumber;
+ }
+ _buffer.Properties[bufferTokenTaggerKey] = new ScanResult(null, newSnapshot, newRegions, null);
}
-
return newRegions;
}
+
/// <summary>
/// Scans "txt" beginning with depth "depth", which is assumed to be non-0. Any occurrences of "/*" or "*/"
/// increment or decrement "depth". If "depth" ever reaches 0, then "end" returns as the number of characters
diff --git a/Source/DafnyExtension/packages.config b/Source/DafnyExtension/packages.config
new file mode 100644
index 00000000..60f856c5
--- /dev/null
+++ b/Source/DafnyExtension/packages.config
@@ -0,0 +1,29 @@
+<?xml version="1.0" encoding="utf-8"?>
+<packages>
+ <package id="VSSDK.ComponentModelHost" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.ComponentModelHost.11" version="11.0.3" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.CoreUtility" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.CoreUtility.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.DTE" version="7.0.4" targetFramework="net45" />
+ <package id="VSSDK.Editor" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.IDE" version="7.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.IDE.10" version="10.0.4" targetFramework="net45" />
+ <package id="VSSDK.IDE.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.IDE.8" version="8.0.4" targetFramework="net45" />
+ <package id="VSSDK.IDE.9" version="9.0.4" targetFramework="net45" />
+ <package id="VSSDK.Language" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.Language.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.OLE.Interop" version="7.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.Shell.Immutable.10" version="10.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.Immutable.11" version="11.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.Interop" version="7.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.Interop.10" version="10.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.Interop.11" version="11.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.Interop.8" version="8.0.4" targetFramework="net45" />
+ <package id="VSSDK.Shell.Interop.9" version="9.0.4" targetFramework="net45" />
+ <package id="VSSDK.Text" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.Text.11" version="11.0.4" targetFramework="net45" developmentDependency="true" />
+ <package id="VSSDK.TextManager.Interop" version="7.0.4" targetFramework="net45" />
+ <package id="VSSDK.TextManager.Interop.8" version="8.0.4" targetFramework="net45" />
+</packages>
diff --git a/Source/DafnyExtension/source.extension.vsixmanifest b/Source/DafnyExtension/source.extension.vsixmanifest
index b87e2452..a3987456 100644
--- a/Source/DafnyExtension/source.extension.vsixmanifest
+++ b/Source/DafnyExtension/source.extension.vsixmanifest
@@ -7,10 +7,11 @@
<License>Z3-LICENSE.txt</License>
</Metadata>
<Installation InstalledByMsi="false">
- <InstallationTarget Version="[11.0,13.0)" Id="Microsoft.VisualStudio.Pro" />
+ <InstallationTarget Version="[11.0,15.0)" Id="Microsoft.VisualStudio.Pro" />
+ <InstallationTarget Version="[14.0,15.0)" Id="Microsoft.VisualStudio.Community" />
</Installation>
<Dependencies>
- <Dependency Id="Microsoft.Framework.NDP" DisplayName="Microsoft .NET Framework" d:Source="Manual" Version="4.5" />
+ <Dependency Id="Microsoft.Framework.NDP" DisplayName="Microsoft .NET Framework" d:Source="Manual" Version="[4.5,]" />
<Dependency Id="Microsoft.VisualStudio.MPF.11.0" DisplayName="Visual Studio MPF 11.0" d:Source="Installed" Version="11.0" />
</Dependencies>
<Assets>
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 23:18:56 +0000