diff options
| author |  rustanleino <unknown> | 2010-10-27 01:06:32 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-10-27 01:06:32 +0000 |
| commit | e2e52528b7232ff95c2bbecd73e35207fd38e121 (patch) | |
| tree | 196b7632f915461be7b7f7baea426a951120e592 /Util | |
| parent | cd2643c9f8b6069771e0e9ab5ff9f33f975ae4f8 (diff) | |
Dafny: Record source positions of start/end curly braces for declaration constructs.
Dafny VS2010 extension: link with Dafny and use it to parse and type check
Diffstat (limited to 'Util')
6 files changed, 854 insertions, 190 deletions
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs new file mode 100644 index 00000000..3c2393bb --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs @@ -0,0 +1,452 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.IO;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+// Here come the Dafny/Boogie specific imports
+//using PureCollections;
+using Microsoft.Boogie;
+using Dafny = Microsoft.Dafny;
+using Microsoft.Boogie.AbstractInterpretation;
+using VC;
+// using AI = Microsoft.AbstractInterpretationFramework;
+
+
+namespace DafnyLanguage
+{
+ class DafnyDriver
+ {
+ readonly string _programText;
+ readonly string _filename;
+ Dafny.Program _program;
+ List<DafnyError> _errors = new List<DafnyError>();
+ public List<DafnyError> Errors { get { return _errors; } }
+
+ public DafnyDriver(string programText, string filename) {
+ _programText = programText;
+ _filename = filename;
+ }
+
+ void RecordError(int line, int col, ErrorCategory cat, string msg) {
+ _errors.Add(new DafnyError(line, col, cat, msg));
+ }
+
+ void RecordProcessError(string msg) {
+ RecordError(0, 0, ErrorCategory.ProcessError, msg);
+ }
+
+ public void Process_ViaBatchFile() {
+ if (!File.Exists(@"C:\tmp\StartDafny.bat")) {
+ RecordProcessError(@"Can't find C:\tmp\StartDafny.bat");
+ }
+
+ // From: http://dotnetperls.com/process-redirect-standard-output
+ // (Also, see: http://msdn.microsoft.com/en-us/library/system.diagnostics.processstartinfo.redirectstandardoutput.aspx)
+ //
+ // Setup the process with the ProcessStartInfo class.
+ //
+ ProcessStartInfo start = new ProcessStartInfo();
+ start.FileName = @"cmd.exe";
+ start.Arguments = @"/c C:\tmp\StartDafny.bat"; // Specify exe name.
+ start.UseShellExecute = false;
+ start.RedirectStandardInput = true;
+ start.RedirectStandardOutput = true;
+ start.CreateNoWindow = true;
+ //
+ // Start the process.
+ //
+ using (System.Diagnostics.Process process = System.Diagnostics.Process.Start(start)) {
+ //
+ // Push the file contents to the new process
+ //
+ StreamWriter myStreamWriter = process.StandardInput;
+ myStreamWriter.WriteLine(_programText);
+ myStreamWriter.Close();
+ //
+ // Read in all the text from the process with the StreamReader.
+ //
+ using (StreamReader reader = process.StandardOutput) {
+ for (string line = reader.ReadLine(); !String.IsNullOrEmpty(line); line = reader.ReadLine()) {
+ // the lines of interest have the form "filename(line,col): some_error_label: error_message"
+ // where "some_error_label" is "Error" or "syntax error" or "Error BP5003" or "Related location"
+ string message;
+ int n = line.IndexOf("): ", 2); // we start at 2, to avoid problems with "C:\..."
+ if (n == -1) {
+ continue;
+ } else {
+ int m = line.IndexOf(": ", n + 3);
+ if (m == -1) {
+ continue;
+ }
+ message = line.Substring(m + 2);
+ }
+ line = line.Substring(0, n); // line now has the form "filename(line,col"
+
+ n = line.LastIndexOf(',');
+ if (n == -1) { continue; }
+ var colString = line.Substring(n + 1);
+ line = line.Substring(0, n); // line now has the form "filename(line"
+
+ n = line.LastIndexOf('(');
+ if (n == -1) { continue; }
+ var lineString = line.Substring(n + 1);
+
+ try {
+ int errLine = Int32.Parse(lineString) - 1;
+ int errCol = Int32.Parse(colString) - 1;
+ RecordError(errLine, errCol, message.StartsWith("syntax error") ? ErrorCategory.ParseError : ErrorCategory.VerificationError, message);
+ } catch (System.FormatException) {
+ continue;
+ } catch (System.OverflowException) {
+ continue;
+ }
+ }
+ }
+ }
+ }
+
+ static DafnyDriver() {
+ Initialize();
+ }
+
+ static void Initialize() {
+ CommandLineOptions.Clo.RunningBoogieOnSsc = false;
+ CommandLineOptions.Clo.TheProverFactory = ProverFactory.Load("Z3");
+ CommandLineOptions.Clo.ProverName = "Z3";
+ CommandLineOptions.Clo.vcVariety = CommandLineOptions.Clo.TheProverFactory.DefaultVCVariety;
+ }
+
+ public Dafny.Program Process() {
+ if (!ParseAndTypeCheck()) {
+ return null;
+ }
+ return _program;
+ }
+
+ bool ParseAndTypeCheck() {
+ List<Dafny.ModuleDecl> modules = new List<Dafny.ModuleDecl>();
+ Dafny.BuiltIns builtIns = new Dafny.BuiltIns();
+ int errorCount = Dafny.Parser.Parse(_programText, _filename, modules, builtIns, new VSErrors(this));
+ if (errorCount != 0)
+ return false;
+ Dafny.Program program = new Dafny.Program(_filename, modules, builtIns);
+
+ Dafny.Resolver r = new VSResolver(program, this);
+ r.ResolveProgram(program);
+ if (r.ErrorCount != 0)
+ return false;
+
+ _program = program;
+ return true; // success
+ }
+
+ class VSErrors : Dafny.Errors
+ {
+ DafnyDriver dd;
+ public VSErrors(DafnyDriver dd) {
+ this.dd = dd;
+ }
+ public override void SynErr(string filename, int line, int col, string msg) {
+ dd.RecordError(line - 1, col - 1, ErrorCategory.ParseError, msg);
+ count++;
+ }
+ public override void SemErr(string filename, int line, int col, string msg) {
+ dd.RecordError(line - 1, col - 1, ErrorCategory.ResolveError, msg);
+ count++;
+ }
+ public override void Warning(string filename, int line, int col, string msg) {
+ dd.RecordError(line - 1, col - 1, ErrorCategory.ParseWarning, msg);
+ }
+ }
+
+ class VSResolver : Dafny.Resolver
+ {
+ DafnyDriver dd;
+ public VSResolver(Dafny.Program program, DafnyDriver dd)
+ : base(program) {
+ this.dd = dd;
+ }
+ protected override void Error(IToken tok, string msg, params object[] args) {
+ string s = string.Format(msg, args);
+ dd.RecordError(tok.line - 1, tok.col - 1, ErrorCategory.ResolveError, s);
+ ErrorCount++;
+ }
+ }
+
+#if LATER
+ static bool Verify(Microsoft.Dafny.Program dafnyProgram) {
+ Dafny.Translator translator = new Dafny.Translator();
+ Program boogieProgram = translator.Translate(dafnyProgram);
+
+ int errorCount, verified, inconclusives, timeOuts, outOfMemories;
+ PipelineOutcome oc = BoogiePipeline(boogieProgram, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
+ switch (oc) {
+ case PipelineOutcome.VerificationCompleted:
+ case PipelineOutcome.Done: // (this says not to continue with compilation)
+ // WriteTrailer(verified, errorCount, inconclusives, timeOuts, outOfMemories);
+ break;
+ default:
+ // error has already been reported to user
+ break;
+ }
+ return errorCount == 0 && inconclusives == 0 && timeOuts == 0 && outOfMemories == 0;
+ }
+
+ /// <summary>
+ /// Resolve, type check, infer invariants for, and verify the given Boogie program.
+ /// The intention is that this Boogie program has been produced by translation from something
+ /// else. Hence, any resolution errors and type checking errors are due to errors in
+ /// the translation.
+ /// </summary>
+ static PipelineOutcome BoogiePipeline(Program/*!*/ program,
+ out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories) {
+ Contract.Requires(program != null);
+ Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));
+
+ errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;
+ PipelineOutcome oc = ResolveAndTypecheck(program);
+ switch (oc) {
+ case PipelineOutcome.Done:
+ return oc;
+
+ case PipelineOutcome.ResolutionError:
+ case PipelineOutcome.TypeCheckingError:
+ // the Dafny-to-Boogie translation must have been bad; this is an internal error
+ return oc;
+
+ case PipelineOutcome.ResolvedAndTypeChecked:
+ return InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories);
+
+ default:
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected outcome
+ }
+ }
+
+
+ enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted }
+
+ /// <summary>
+ /// Resolves and type checks the given Boogie program. Any errors are reported to the
+ /// console. Returns:
+ /// - Done if no errors occurred, and command line specified no resolution or no type checking.
+ /// - ResolutionError if a resolution error occurred
+ /// - TypeCheckingError if a type checking error occurred
+ /// - ResolvedAndTypeChecked if both resolution and type checking succeeded
+ /// </summary>
+ static PipelineOutcome ResolveAndTypecheck(Program program) {
+ Contract.Requires(program != null);
+ // ---------- Resolve ------------------------------------------------------------
+
+ int errorCount = program.Resolve();
+ if (errorCount != 0) {
+ return PipelineOutcome.ResolutionError;
+ }
+
+ // ---------- Type check ------------------------------------------------------------
+
+ errorCount = program.Typecheck();
+ if (errorCount != 0) {
+ return PipelineOutcome.TypeCheckingError;
+ }
+
+ return PipelineOutcome.ResolvedAndTypeChecked;
+ }
+
+ /// <summary>
+ /// Given a resolved and type checked Boogie program, infers invariants for the program
+ /// and then attempts to verify it. Returns:
+ /// - Done if command line specified no verification
+ /// - FatalError if a fatal error occurred, in which case an error has been printed to console
+ /// - VerificationCompleted if inference and verification completed, in which the out
+ /// parameters contain meaningful values
+ /// </summary>
+ static PipelineOutcome InferAndVerify(Program program,
+ out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories) {
+ Contract.Requires(program != null);
+ Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));
+
+ errorCount = verified = inconclusives = timeOuts = outOfMemories = 0;
+
+ // ---------- Infer invariants --------------------------------------------------------
+
+ // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
+ Microsoft.Boogie.AbstractInterpretation.AbstractInterpretation.RunAbstractInterpretation(program);
+
+ if (CommandLineOptions.Clo.ExpandLambdas) {
+ LambdaHelper.ExpandLambdas(program);
+ }
+
+ // ---------- Verify ------------------------------------------------------------
+
+ #region Verify each implementation
+
+ ConditionGeneration vcgen = null;
+ try {
+ if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {
+ vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ } else {
+ vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);
+ }
+ } catch (ProverException e) {
+ ErrorWriteLine("Fatal Error: ProverException: {0}", e);
+ return PipelineOutcome.FatalError;
+ }
+
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ Contract.Assert(decl != null);
+ Implementation impl = decl as Implementation;
+ if (impl != null && CommandLineOptions.Clo.UserWantsToCheckRoutine(cce.NonNull(impl.Name)) && !impl.SkipVerification) {
+ List<Counterexample>/*?*/ errors;
+
+ DateTime start = new DateTime(); // to please compiler's definite assignment rules
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {
+ start = DateTime.Now;
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine();
+ Console.WriteLine("Verifying {0} ...", impl.Name);
+ }
+ if (CommandLineOptions.Clo.XmlSink != null) {
+ CommandLineOptions.Clo.XmlSink.WriteStartMethod(impl.Name, start);
+ }
+ }
+
+ ConditionGeneration.Outcome outcome;
+ try {
+ outcome = vcgen.VerifyImplementation(impl, program, out errors);
+ } catch (VCGenException e) {
+ ReportBplError(impl, String.Format("Error BP5010: {0} Encountered in implementation {1}.", e.Message, impl.Name), true);
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ } catch (UnexpectedProverOutputException upo) {
+ AdvisoryWriteLine("Advisory: {0} SKIPPED because of internal error: unexpected prover output: {1}", impl.Name, upo.Message);
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ }
+
+ string timeIndication = "";
+ DateTime end = DateTime.Now;
+ TimeSpan elapsed = end - start;
+ if (CommandLineOptions.Clo.Trace || CommandLineOptions.Clo.XmlSink != null) {
+ if (CommandLineOptions.Clo.Trace) {
+ timeIndication = string.Format(" [{0} s] ", elapsed.TotalSeconds);
+ }
+ }
+
+
+ switch (outcome) {
+ default:
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected outcome
+ case VCGen.Outcome.Correct:
+ Inform(String.Format("{0}verified", timeIndication));
+ verified++;
+ break;
+ case VCGen.Outcome.TimedOut:
+ timeOuts++;
+ Inform(String.Format("{0}timed out", timeIndication));
+ break;
+ case VCGen.Outcome.OutOfMemory:
+ outOfMemories++;
+ Inform(String.Format("{0}out of memory", timeIndication));
+ break;
+ case VCGen.Outcome.Inconclusive:
+ inconclusives++;
+ Inform(String.Format("{0}inconclusive", timeIndication));
+ break;
+ case VCGen.Outcome.Errors:
+ Contract.Assert(errors != null); // guaranteed by postcondition of VerifyImplementation
+ // BP1xxx: Parsing errors
+ // BP2xxx: Name resolution errors
+ // BP3xxx: Typechecking errors
+ // BP4xxx: Abstract interpretation errors (Is there such a thing?)
+ // BP5xxx: Verification errors
+
+ errors.Sort(new CounterexampleComparer());
+ foreach (Counterexample error in errors) {
+ if (error is CallCounterexample) {
+ CallCounterexample err = (CallCounterexample)error;
+ ReportBplError(err.FailingCall, "Error BP5002: A precondition for this call might not hold.", true);
+ ReportBplError(err.FailingRequires, "Related location: This is the precondition that might not hold.", false);
+ } else if (error is ReturnCounterexample) {
+ ReturnCounterexample err = (ReturnCounterexample)error;
+ ReportBplError(err.FailingReturn, "Error BP5003: A postcondition might not hold on this return path.", true);
+ ReportBplError(err.FailingEnsures, "Related location: This is the postcondition that might not hold.", false);
+ } else // error is AssertCounterexample
+ {
+ AssertCounterexample err = (AssertCounterexample)error;
+ if (err.FailingAssert is LoopInitAssertCmd) {
+ ReportBplError(err.FailingAssert, "Error BP5004: This loop invariant might not hold on entry.", true);
+ } else if (err.FailingAssert is LoopInvMaintainedAssertCmd) {
+ // this assertion is a loop invariant which is not maintained
+ ReportBplError(err.FailingAssert, "Error BP5005: This loop invariant might not be maintained by the loop.", true);
+ } else {
+ string msg = err.FailingAssert.ErrorData as string;
+ if (msg == null) {
+ msg = "Error BP5001: This assertion might not hold.";
+ }
+ ReportBplError(err.FailingAssert, msg, true);
+ }
+ }
+ if (CommandLineOptions.Clo.ErrorTrace > 0) {
+ Console.WriteLine("Execution trace:");
+ foreach (Block b in error.Trace) {
+ Contract.Assert(b != null);
+ if (b.tok == null) {
+ Console.WriteLine(" <intermediate block>");
+ } else {
+ // for ErrorTrace == 1 restrict the output;
+ // do not print tokens with -17:-4 as their location because they have been
+ // introduced in the translation and do not give any useful feedback to the user
+ if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) {
+ Console.WriteLine(" {0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label);
+ }
+ }
+ }
+ }
+ errorCount++;
+ }
+ Inform(String.Format("{0}error{1}", timeIndication, errors.Count == 1 ? "" : "s"));
+ break;
+ }
+ if (outcome == VCGen.Outcome.Errors || CommandLineOptions.Clo.Trace) {
+ Console.Out.Flush();
+ }
+ }
+ }
+ vcgen.Close();
+ cce.NonNull(CommandLineOptions.Clo.TheProverFactory).Close();
+
+ #endregion
+
+ return PipelineOutcome.VerificationCompleted;
+ }
+
+ static void ReportBplError(Absy node, string message, bool error) {
+ Contract.Requires(node != null); Contract.Requires(message != null);
+ IToken tok = node.tok;
+ string s;
+ if (tok == null) {
+ s = message;
+ } else {
+ s = string.Format("{0}({1},{2}): {3}", tok.filename, tok.line, tok.col, message);
+ }
+ if (error) {
+ ErrorWriteLine(s);
+ } else {
+ Console.WriteLine(s);
+ }
+ }
+
+ /// <summary>
+ /// Inform the user about something and proceed with translation normally.
+ /// Print newline after the message.
+ /// </summary>
+ public static void Inform(string s) {
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine(s);
+ }
+ }
+#endif
+ }
+}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj index f6320284..dedb141e 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj @@ -33,6 +33,57 @@ <WarningLevel>4</WarningLevel>
</PropertyGroup>
<ItemGroup>
+ <Reference Include="AbsInt, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\AbsInt.dll</HintPath>
+ </Reference>
+ <Reference Include="AIFramework, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\AIFramework.dll</HintPath>
+ </Reference>
+ <Reference Include="Basetypes, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\Basetypes.dll</HintPath>
+ </Reference>
+ <Reference Include="CodeContractsExtender, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\CodeContractsExtender.dll</HintPath>
+ </Reference>
+ <Reference Include="Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\Core.dll</HintPath>
+ </Reference>
+ <Reference Include="DafnyPipeline, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\DafnyPipeline.dll</HintPath>
+ </Reference>
+ <Reference Include="FSharp.Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\FSharp.Core.dll</HintPath>
+ </Reference>
+ <Reference Include="FSharp.PowerPack, Version=1.9.9.9, Culture=neutral, PublicKeyToken=a19089b1c74d0809, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\FSharp.PowerPack.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\Microsoft.Contracts.dll</HintPath>
+ </Reference>
+ <Reference Include="Provers.Z3">
+ <HintPath>..\..\..\..\Binaries\Provers.Z3.dll</HintPath>
+ </Reference>
+ <Reference Include="VCGeneration, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\VCGeneration.dll</HintPath>
+ </Reference>
+ <Reference Include="System.Compiler, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\Binaries\System.Compiler.dll</HintPath>
+ </Reference>
+ <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\Binaries\System.Compiler.Runtime.dll</HintPath>
+ </Reference>
<Reference Include="EnvDTE, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
<EmbedInteropTypes>False</EmbedInteropTypes>
</Reference>
@@ -79,6 +130,9 @@ </ItemGroup>
<ItemGroup>
<Compile Include="BufferIdleEventUtil.cs" />
+ <Compile Include="OutliningTagger.cs" />
+ <Compile Include="ResolverTagger.cs" />
+ <Compile Include="DafnyDriver.cs" />
<Compile Include="ContentType.cs" />
<Compile Include="BraceMatching.cs" />
<Compile Include="WordHighlighter.cs" />
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ErrorTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ErrorTagger.cs index 393aa8c8..efd755d8 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ErrorTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ErrorTagger.cs @@ -18,8 +18,6 @@ using Microsoft.VisualStudio.Text.Editor; using Microsoft.VisualStudio.Text.Tagging;
using Microsoft.VisualStudio.Text.Projection;
using Microsoft.VisualStudio.Utilities;
-using System.Diagnostics;
-using System.IO;
namespace DafnyLanguage
{
@@ -28,15 +26,13 @@ namespace DafnyLanguage [TagType(typeof(ErrorTag))]
internal sealed class ErrorTaggerProvider : ITaggerProvider
{
- [Import(typeof(Microsoft.VisualStudio.Shell.SVsServiceProvider))]
- internal IServiceProvider _serviceProvider = null;
-
[Import]
- ITextDocumentFactoryService _textDocumentFactory = null;
+ internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+ ITagAggregator<DafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyResolverTag>(buffer);
// create a single tagger for each buffer.
- Func<ITagger<T>> sc = delegate() { return new ErrorTagger(buffer, _serviceProvider, _textDocumentFactory) as ITagger<T>; };
+ Func<ITagger<T>> sc = delegate() { return new ErrorTagger(buffer, tagAggregator) as ITagger<T>; };
return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
}
}
@@ -44,31 +40,15 @@ namespace DafnyLanguage /// <summary>
/// Translate PkgDefTokenTags into ErrorTags and Error List items
/// </summary>
- internal sealed class ErrorTagger : ITagger<ErrorTag>, IDisposable
+ internal sealed class ErrorTagger : ITagger<ErrorTag>
{
ITextBuffer _buffer;
- ITextDocument _document;
- ITextSnapshot _snapshot; // may be null
- List<DafnyError> _errors = new List<DafnyError>();
- ErrorListProvider _errorProvider;
+ ITagAggregator<DafnyResolverTag> _aggregator;
- internal ErrorTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory) {
+ internal ErrorTagger(ITextBuffer buffer, ITagAggregator<DafnyResolverTag> tagAggregator) {
_buffer = buffer;
- if (!textDocumentFactory.TryGetTextDocument(_buffer, out _document))
- _document = null;
- _snapshot = null; // this makes sure the next snapshot will look different
- _errorProvider = new ErrorListProvider(serviceProvider);
-
- // ProcessFile(null, EventArgs.Empty);
- BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ProcessFile);
- }
-
- public void Dispose() {
- if (_errorProvider != null) {
- _errorProvider.Tasks.Clear();
- _errorProvider.Dispose();
- }
- BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ProcessFile);
+ _aggregator = tagAggregator;
+ _aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
}
/// <summary>
@@ -77,28 +57,13 @@ namespace DafnyLanguage public IEnumerable<ITagSpan<ErrorTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
if (spans.Count == 0) yield break;
var snapshot = spans[0].Snapshot;
-
- foreach (var err in _errors) {
- if (err.Category != ErrorCategory.ProcessError) {
- var line = snapshot.GetLineFromLineNumber(err.Line);
- var length = line.Length - err.Column;
- if (5 < length) length = 5;
- SnapshotSpan span = new SnapshotSpan(new SnapshotPoint(snapshot, line.Start.Position + err.Column), length);
- // http://msdn.microsoft.com/en-us/library/dd885244.aspx says one can use the error types below, but they
- // all show as purple squiggles for me. And just "error" (which is not mentioned on that page) shows up
- // as red.
- string ty;
- switch (err.Category) {
- default: // unexpected category
- case ErrorCategory.ParseError:
- // ty = "syntax error";
- ty = "error"; break;
- case ErrorCategory.ResolveError:
- ty = "compiler error"; break;
- case ErrorCategory.VerificationError:
- ty = "other error"; break;
+ foreach (var tagSpan in this._aggregator.GetTags(spans)) {
+ DafnyResolverTag t = tagSpan.Tag;
+ DafnyErrorResolverTag et = t as DafnyErrorResolverTag;
+ if (et != null) {
+ foreach (SnapshotSpan s in tagSpan.Span.GetSpans(snapshot)) {
+ yield return new TagSpan<ErrorTag>(s, new ErrorTag(et.Typ, et.Msg));
}
- yield return new TagSpan<ErrorTag>(span, new ErrorTag(ty, err.Message));
}
}
}
@@ -106,150 +71,15 @@ namespace DafnyLanguage // the Classifier tagger is translating buffer change events into TagsChanged events, so we don't have to
public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
- /// <summary>
- /// Calls the Dafny verifier on the program, updates the Error List accordingly.
- /// </summary>
- void ProcessFile(object sender, EventArgs args) {
- ITextSnapshot snapshot = _buffer.CurrentSnapshot;
- if (snapshot == _snapshot)
- return; // we've already done this snapshot
- NormalizedSnapshotSpanCollection spans = new NormalizedSnapshotSpanCollection(new SnapshotSpan(snapshot, 0, snapshot.Length));
-
- var newErrors = Verify(_buffer.CurrentSnapshot.GetText());
-
- _errorProvider.Tasks.Clear();
- foreach (var err in newErrors) {
- ErrorTask task = new ErrorTask();
- task.CanDelete = true;
- task.Category = TaskCategory.BuildCompile;
- if (_document != null)
- task.Document = _document.FilePath;
- task.ErrorCategory = TaskErrorCategory.Error;
- task.Text = err.Message;
- if (err.Category != ErrorCategory.ProcessError) {
- task.Line = err.Line;
- task.Column = err.Column;
- task.Navigate += new EventHandler(task_Navigate);
- }
- _errorProvider.Tasks.Add(task);
- }
-
- _errors = newErrors;
- _snapshot = snapshot;
+ void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {
var chng = TagsChanged;
- if (chng != null)
- chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));
- }
-
- private static List<DafnyError> Verify(string theProgram) {
- List<DafnyError> errors = new List<DafnyError>();
-
- if (!File.Exists(@"C:\tmp\StartDafny.bat")) {
- RecordError(errors, 0, 0, ErrorCategory.ProcessError, @"Can't find C:\tmp\StartDafny.bat");
- return errors;
- }
-
- // From: http://dotnetperls.com/process-redirect-standard-output
- // (Also, see: http://msdn.microsoft.com/en-us/library/system.diagnostics.processstartinfo.redirectstandardoutput.aspx)
- //
- // Setup the process with the ProcessStartInfo class.
- //
- ProcessStartInfo start = new ProcessStartInfo();
- start.FileName = @"cmd.exe";
- start.Arguments = @"/c C:\tmp\StartDafny.bat"; // Specify exe name.
- start.UseShellExecute = false;
- start.RedirectStandardInput = true;
- start.RedirectStandardOutput = true;
- start.CreateNoWindow = true;
- //
- // Start the process.
- //
- using (System.Diagnostics.Process process = System.Diagnostics.Process.Start(start)) {
- //
- // Push the file contents to the new process
- //
- StreamWriter myStreamWriter = process.StandardInput;
- myStreamWriter.WriteLine(theProgram);
- myStreamWriter.Close();
- //
- // Read in all the text from the process with the StreamReader.
- //
- using (StreamReader reader = process.StandardOutput) {
- for (string line = reader.ReadLine(); !String.IsNullOrEmpty(line); line = reader.ReadLine()) {
- // the lines of interest have the form "filename(line,col): some_error_label: error_message"
- // where "some_error_label" is "Error" or "syntax error" or "Error BP5003" or "Related location"
- string message;
- int n = line.IndexOf("): ", 2); // we start at 2, to avoid problems with "C:\..."
- if (n == -1) {
- continue;
- } else {
- int m = line.IndexOf(": ", n + 3);
- if (m == -1) {
- continue;
- }
- message = line.Substring(m + 2);
- }
- line = line.Substring(0, n); // line now has the form "filename(line,col"
-
- n = line.LastIndexOf(',');
- if (n == -1) { continue; }
- var colString = line.Substring(n + 1);
- line = line.Substring(0, n); // line now has the form "filename(line"
-
- n = line.LastIndexOf('(');
- if (n == -1) { continue; }
- var lineString = line.Substring(n + 1);
-
- try {
- int errLine = Int32.Parse(lineString) - 1;
- int errCol = Int32.Parse(colString) - 1;
- RecordError(errors, errLine, errCol, message.StartsWith("syntax error") ? ErrorCategory.ParseError : ErrorCategory.VerificationError, message);
- } catch (System.FormatException) {
- continue;
- } catch (System.OverflowException) {
- continue;
- }
- }
+ if (chng != null) {
+ NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);
+ if (spans.Count > 0) {
+ SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);
+ chng(this, new SnapshotSpanEventArgs(span));
}
}
- return errors;
- }
-
- private static void RecordError(List<DafnyError> errors, int line, int col, ErrorCategory cat, string msg) {
- errors.Add(new DafnyError(line, col, cat, msg));
- }
-
- /// <summary>
- /// Callback method attached to each of our tasks in the Error List
- /// </summary>
- void task_Navigate(object sender, EventArgs e) {
- ErrorTask error = sender as ErrorTask;
- if (error != null) {
- error.Line += 1;
- error.Column += 1;
- _errorProvider.Navigate(error, new Guid(EnvDTE.Constants.vsViewKindCode));
- error.Column -= 1;
- error.Line -= 1;
- }
- }
- }
-
- public enum ErrorCategory
- {
- ProcessError, ParseError, ResolveError, VerificationError
- }
-
- internal class DafnyError
- {
- public readonly int Line; // 0 based
- public readonly int Column; // 0 based
- public readonly ErrorCategory Category;
- public readonly string Message;
- public DafnyError(int line, int col, ErrorCategory cat, string msg) {
- Line = line;
- Column = col;
- Category = cat;
- Message = msg;
}
}
}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs b/Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs index 3fbcb054..3e64e43d 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs @@ -12,6 +12,7 @@ using Microsoft.VisualStudio.Text; namespace DafnyLanguage
{
+#if THIS_IS_THE_PAST
[Export(typeof(ITaggerProvider))]
[ContentType("dafny")]
[TagType(typeof(IOutliningRegionTag))]
@@ -217,4 +218,5 @@ namespace DafnyLanguage NormalizedSnapshotSpanCollection.Difference(second, first));
}
}
+#endif
}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs new file mode 100644 index 00000000..acd357b1 --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs @@ -0,0 +1,118 @@ +//***************************************************************************
+// Copyright © 2010 Microsoft Corporation. All Rights Reserved.
+// This code released under the terms of the
+// Microsoft Public License (MS-PL, http://opensource.org/licenses/ms-pl.html.)
+//***************************************************************************
+using EnvDTE;
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.ComponentModel.Composition;
+using System.Windows.Threading;
+using Microsoft.VisualStudio.Shell;
+using Microsoft.VisualStudio.Shell.Interop;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Classification;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Text.Projection;
+using Microsoft.VisualStudio.Utilities;
+using Bpl = Microsoft.Boogie;
+using Dafny = Microsoft.Dafny;
+
+namespace DafnyLanguage
+{
+ [Export(typeof(ITaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(IOutliningRegionTag))]
+ internal sealed class OutliningTaggerProvider : ITaggerProvider
+ {
+ [Import]
+ internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
+
+ public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+ ITagAggregator<DafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyResolverTag>(buffer);
+ // create a single tagger for each buffer.
+ Func<ITagger<T>> sc = delegate() { return new OutliningTagger(buffer, tagAggregator) as ITagger<T>; };
+ return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
+ }
+ }
+
+ /// <summary>
+ /// Translate PkgDefTokenTags into ErrorTags and Error List items
+ /// </summary>
+ internal sealed class OutliningTagger : ITagger<IOutliningRegionTag>
+ {
+ ITextBuffer _buffer;
+ ITagAggregator<DafnyResolverTag> _aggregator;
+
+ internal OutliningTagger(ITextBuffer buffer, ITagAggregator<DafnyResolverTag> tagAggregator) {
+ _buffer = buffer;
+ _aggregator = tagAggregator;
+ _aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
+ }
+
+ /// <summary>
+ /// Find the Error tokens in the set of all tokens and create an ErrorTag for each
+ /// </summary>
+ public IEnumerable<ITagSpan<IOutliningRegionTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+ if (spans.Count == 0) yield break;
+ var snapshot = spans[0].Snapshot;
+ foreach (var tagSpan in this._aggregator.GetTags(spans)) {
+ DafnyResolverTag t = tagSpan.Tag;
+ DafnySuccessResolverTag st = t as DafnySuccessResolverTag;
+ if (st != null) {
+ foreach (Dafny.ModuleDecl module in st.Program.Modules) {
+ if (!module.IsDefaultModule) {
+ yield return GetOutliningRegionTag(snapshot, module, "module");
+ }
+ foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) {
+ if (d is Dafny.DatatypeDecl) {
+ yield return GetOutliningRegionTag(snapshot, d, "datatype");
+ } else {
+ Dafny.ClassDecl cl = (Dafny.ClassDecl)d;
+ if (!cl.IsDefaultClass) {
+ yield return GetOutliningRegionTag(snapshot, cl, "class");
+ }
+ // do the class members (in particular, functions and methods)
+ foreach (Dafny.MemberDecl m in cl.Members) {
+ if (m is Dafny.Function && ((Dafny.Function)m).Body != null) {
+ yield return GetOutliningRegionTag(snapshot, m, "function");
+ } else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) {
+ yield return GetOutliningRegionTag(snapshot, m, "method");
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
+ TagSpan<OutliningRegionTag> GetOutliningRegionTag(ITextSnapshot snapshot, Dafny.Declaration decl, string kind) {
+ int startPosition = decl.BodyStartTok.pos + 1; // skip the open-curly brace itself
+ int length = decl.BodyEndTok.pos - startPosition;
+ return new TagSpan<OutliningRegionTag>(
+ new SnapshotSpan(snapshot, startPosition, length),
+ new OutliningRegionTag(false, false, "...", string.Format("body of {0} {1}", kind, decl.Name)));
+ }
+
+ // the Classifier tagger is translating buffer change events into TagsChanged events, so we don't have to
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+ void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {
+ var r = sender as ResolverTagger;
+ if (r != null && r._program != null) {
+ var chng = TagsChanged;
+ if (chng != null) {
+ NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);
+ if (spans.Count > 0) {
+ SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);
+ chng(this, new SnapshotSpanEventArgs(span));
+ }
+ }
+ }
+ }
+ }
+}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs new file mode 100644 index 00000000..1a288ab4 --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs @@ -0,0 +1,208 @@ +//***************************************************************************
+// Copyright © 2010 Microsoft Corporation. All Rights Reserved.
+// This code released under the terms of the
+// Microsoft Public License (MS-PL, http://opensource.org/licenses/ms-pl.html.)
+//***************************************************************************
+using EnvDTE;
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.ComponentModel.Composition;
+using System.Windows.Threading;
+using Microsoft.VisualStudio.Shell;
+using Microsoft.VisualStudio.Shell.Interop;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Classification;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Text.Projection;
+using Microsoft.VisualStudio.Utilities;
+using Dafny = Microsoft.Dafny;
+
+namespace DafnyLanguage
+{
+ [Export(typeof(ITaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(DafnyResolverTag))]
+ internal sealed class ResolverTaggerProvider : ITaggerProvider
+ {
+ [Import(typeof(Microsoft.VisualStudio.Shell.SVsServiceProvider))]
+ internal IServiceProvider _serviceProvider = null;
+
+ [Import]
+ ITextDocumentFactoryService _textDocumentFactory = null;
+
+ public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+ // create a single tagger for each buffer.
+ Func<ITagger<T>> sc = delegate() { return new ResolverTagger(buffer, _serviceProvider, _textDocumentFactory) as ITagger<T>; };
+ return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
+ }
+ }
+
+ public abstract class DafnyResolverTag : ITag
+ {
+ }
+ public class DafnyErrorResolverTag : DafnyResolverTag
+ {
+ public readonly string Typ;
+ public readonly string Msg;
+ public DafnyErrorResolverTag(string typ, string msg) {
+ Typ = typ;
+ Msg = msg;
+ }
+ }
+ public class DafnySuccessResolverTag : DafnyResolverTag
+ {
+ public readonly Dafny.Program Program;
+ public DafnySuccessResolverTag(Dafny.Program program) {
+ Program = program;
+ }
+ }
+
+ /// <summary>
+ /// Translate PkgDefTokenTags into ErrorTags and Error List items
+ /// </summary>
+ internal sealed class ResolverTagger : ITagger<DafnyResolverTag>, IDisposable
+ {
+ ITextBuffer _buffer;
+ ITextDocument _document;
+ ITextSnapshot _snapshot; // may be null
+ List<DafnyError> _errors = new List<DafnyError>();
+ ErrorListProvider _errorProvider;
+ public Dafny.Program _program; // non-null only if the snapshot contains a Dafny program that type checks
+
+ internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory) {
+ _buffer = buffer;
+ if (!textDocumentFactory.TryGetTextDocument(_buffer, out _document))
+ _document = null;
+ _snapshot = null; // this makes sure the next snapshot will look different
+ _errorProvider = new ErrorListProvider(serviceProvider);
+
+ BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ProcessFile);
+ }
+
+ public void Dispose() {
+ if (_errorProvider != null) {
+ try {
+ _errorProvider.Tasks.Clear();
+ } catch (InvalidOperationException) {
+ // this may occur if the SVsServiceProvider somehow has been uninstalled before our Dispose method is called
+ }
+ _errorProvider.Dispose();
+ }
+ BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ProcessFile);
+ }
+
+ /// <summary>
+ /// Find the Error tokens in the set of all tokens and create an ErrorTag for each
+ /// </summary>
+ public IEnumerable<ITagSpan<DafnyResolverTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+ if (spans.Count == 0) yield break;
+ var snapshot = spans[0].Snapshot;
+
+ foreach (var err in _errors) {
+ if (err.Category != ErrorCategory.ProcessError) {
+ var line = snapshot.GetLineFromLineNumber(err.Line);
+ var length = line.Length - err.Column;
+ if (5 < length) length = 5;
+ SnapshotSpan span = new SnapshotSpan(new SnapshotPoint(snapshot, line.Start.Position + err.Column), length);
+ // http://msdn.microsoft.com/en-us/library/dd885244.aspx says one can use the error types below, but they
+ // all show as purple squiggles for me. And just "error" (which is not mentioned on that page) shows up
+ // as red.
+ string ty;
+ switch (err.Category) {
+ default: // unexpected category
+ case ErrorCategory.ParseError:
+ // ty = "syntax error";
+ ty = "error"; break;
+ case ErrorCategory.ResolveError:
+ ty = "compiler error"; break;
+ case ErrorCategory.VerificationError:
+ ty = "other error"; break;
+ case ErrorCategory.ParseWarning:
+ ty = "warning"; break;
+ }
+ yield return new TagSpan<DafnyResolverTag>(span, new DafnyErrorResolverTag(ty, err.Message));
+ }
+ }
+ if (_program != null) {
+ yield return new TagSpan<DafnyResolverTag>(new SnapshotSpan(snapshot, 0, snapshot.Length), new DafnySuccessResolverTag(_program));
+ }
+ }
+
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+ /// <summary>
+ /// Calls the Dafny verifier on the program, updates the Error List accordingly.
+ /// </summary>
+ void ProcessFile(object sender, EventArgs args) {
+ ITextSnapshot snapshot = _buffer.CurrentSnapshot;
+ if (snapshot == _snapshot)
+ return; // we've already done this snapshot
+ NormalizedSnapshotSpanCollection spans = new NormalizedSnapshotSpanCollection(new SnapshotSpan(snapshot, 0, snapshot.Length));
+
+ var driver = new DafnyDriver(_buffer.CurrentSnapshot.GetText(), _document != null ? _document.FilePath : "<program>");
+ Dafny.Program program = driver.Process();
+ var newErrors = driver.Errors;
+
+ _errorProvider.Tasks.Clear();
+ foreach (var err in newErrors) {
+ ErrorTask task = new ErrorTask();
+ task.CanDelete = true;
+ task.Category = TaskCategory.BuildCompile;
+ if (_document != null)
+ task.Document = _document.FilePath;
+ task.ErrorCategory = TaskErrorCategory.Error;
+ task.Text = err.Message;
+ if (err.Category != ErrorCategory.ProcessError) {
+ task.Line = err.Line;
+ task.Column = err.Column;
+ task.Navigate += new EventHandler(task_Navigate);
+ }
+ _errorProvider.Tasks.Add(task);
+ }
+
+ _errors = newErrors;
+ _snapshot = snapshot;
+ _program = program;
+ var chng = TagsChanged;
+ if (chng != null)
+ chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));
+ }
+
+ /// <summary>
+ /// Callback method attached to each of our tasks in the Error List
+ /// </summary>
+ void task_Navigate(object sender, EventArgs e) {
+ ErrorTask error = sender as ErrorTask;
+ if (error != null) {
+ error.Line += 1;
+ error.Column += 1;
+ // TODO: how to move the cursor to the right column?
+ _errorProvider.Navigate(error, new Guid(EnvDTE.Constants.vsViewKindCode));
+ error.Column -= 1;
+ error.Line -= 1;
+ }
+ }
+ }
+
+ public enum ErrorCategory
+ {
+ ProcessError, ParseWarning, ParseError, ResolveError, VerificationError
+ }
+
+ internal class DafnyError
+ {
+ public readonly int Line; // 0 based
+ public readonly int Column; // 0 based
+ public readonly ErrorCategory Category;
+ public readonly string Message;
+ public DafnyError(int line, int col, ErrorCategory cat, string msg) {
+ Line = line;
+ Column = col;
+ Category = cat;
+ Message = msg;
+ }
+ }
+}
|