DafnyExtension: Did some refactoring.

16 files changed, 267 insertions, 152 deletions

diff --git a/Source/DafnyExtension/BraceMatching.cs b/Source/DafnyExtension/BraceMatching.cs
index 44b1affe..50d264ef 100644
--- a/Source/DafnyExtension/BraceMatching.cs
+++ b/Source/DafnyExtension/BraceMatching.cs
@@ -1,5 +1,4 @@
 using System;

-using System.Linq;

 using System.Collections.Generic;

 using System.ComponentModel.Composition;

 using Microsoft.VisualStudio.Text;

@@ -7,8 +6,12 @@ using Microsoft.VisualStudio.Text.Editor;
 using Microsoft.VisualStudio.Text.Tagging;

 using Microsoft.VisualStudio.Utilities;

 

+

 namespace DafnyLanguage

 {

+

+  #region Provider

+

   [Export(typeof(IViewTaggerProvider))]

   [ContentType("dafny")]

   [TagType(typeof(TextMarkerTag))]

@@ -30,6 +33,11 @@ namespace DafnyLanguage
     }

   }

 

+  #endregion

+

+

+  #region Tagger

+

   internal abstract class TokenBasedTagger

   {

     ITagAggregator<DafnyTokenTag> _aggregator;

@@ -42,8 +50,8 @@ namespace DafnyLanguage
       SnapshotSpan span = new SnapshotSpan(pt, 1);

       foreach (var tagSpan in this._aggregator.GetTags(span)) {

         switch (tagSpan.Tag.Kind) {

-          case DafnyTokenKinds.Comment:

-          case DafnyTokenKinds.String:

+          case DafnyTokenKind.Comment:

+          case DafnyTokenKind.String:

             foreach (var s in tagSpan.Span.GetSpans(pt.Snapshot)) {

               if (s.Contains(span))

                 return true;

@@ -57,6 +65,7 @@ namespace DafnyLanguage
     }

   }

 

+

   internal class BraceMatchingTagger : TokenBasedTagger, ITagger<TextMarkerTag>

   {

     ITextView View { get; set; }

@@ -250,4 +259,7 @@ namespace DafnyLanguage
       return false;

     }

   }

+

+  #endregion

+

 }

diff --git a/Source/DafnyExtension/BufferIdleEventUtil.cs b/Source/DafnyExtension/BufferIdleEventUtil.cs
index 1aea1385..8a1ad0ed 100644
--- a/Source/DafnyExtension/BufferIdleEventUtil.cs
+++ b/Source/DafnyExtension/BufferIdleEventUtil.cs
@@ -1,17 +1,19 @@
 //***************************************************************************

 // Copyright © 2010 Microsoft Corporation.  All Rights Reserved.

-// This code released under the terms of the 

+// This code released under the terms of the

 // Microsoft Public License (MS-PL, http://opensource.org/licenses/ms-pl.html.)

 //***************************************************************************

+

+

 using System;

 using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using Microsoft.VisualStudio.Text;

 using System.Windows.Threading;

+using Microsoft.VisualStudio.Text;

+

 

 namespace DafnyLanguage

 {

+

     /// <summary>

     /// Handy reusable utility to listen for change events on the associated buffer, but

     /// only pass these along to a set of listeners when the user stops typing for a half second

@@ -152,4 +154,5 @@ namespace DafnyLanguage
 

         #endregion

     }

+

 }

diff --git a/Source/DafnyExtension/ClassificationTagger.cs b/Source/DafnyExtension/ClassificationTagger.cs
index 8f6191e5..b3bafa11 100644
--- a/Source/DafnyExtension/ClassificationTagger.cs
+++ b/Source/DafnyExtension/ClassificationTagger.cs
@@ -4,13 +4,15 @@ using System.ComponentModel.Composition;
 using System.Windows.Media;

 using Microsoft.VisualStudio.Text;

 using Microsoft.VisualStudio.Text.Classification;

-using Microsoft.VisualStudio.Text.Editor;

 using Microsoft.VisualStudio.Text.Tagging;

 using Microsoft.VisualStudio.Utilities;

 

 

 namespace DafnyLanguage

 {

+

+  #region Provider

+

   [Export(typeof(ITaggerProvider))]

   [ContentType("dafny")]

   [TagType(typeof(ClassificationTag))]

@@ -31,11 +33,15 @@ namespace DafnyLanguage
     }

   }

 

+  #endregion

+

+  #region Tagger

+

   internal sealed class DafnyClassifier : ITagger<ClassificationTag>

   {

     ITextBuffer _buffer;

     ITagAggregator<DafnyTokenTag> _aggregator;

-    IDictionary<DafnyTokenKinds, IClassificationType> _typeMap;

+    IDictionary<DafnyTokenKind, IClassificationType> _typeMap;

 

     static bool DafnyMenuWasInitialized;

 

@@ -45,14 +51,15 @@ namespace DafnyLanguage
       _buffer = buffer;

       _aggregator = tagAggregator;

       _aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);

+

       // use built-in classification types:

-      _typeMap = new Dictionary<DafnyTokenKinds, IClassificationType>();

-      _typeMap[DafnyTokenKinds.Keyword] = standards.Keyword;

-      _typeMap[DafnyTokenKinds.Number] = standards.NumberLiteral;

-      _typeMap[DafnyTokenKinds.String] = standards.StringLiteral;

-      _typeMap[DafnyTokenKinds.Comment] = standards.Comment;

-      _typeMap[DafnyTokenKinds.VariableIdentifier] = standards.Identifier;

-      _typeMap[DafnyTokenKinds.VariableIdentifierDefinition] = typeService.GetClassificationType("Dafny identifier");

+      _typeMap = new Dictionary<DafnyTokenKind, IClassificationType>();

+      _typeMap[DafnyTokenKind.Keyword] = standards.Keyword;

+      _typeMap[DafnyTokenKind.Number] = standards.NumberLiteral;

+      _typeMap[DafnyTokenKind.String] = standards.StringLiteral;

+      _typeMap[DafnyTokenKind.Comment] = standards.Comment;

+      _typeMap[DafnyTokenKind.VariableIdentifier] = standards.Identifier;

+      _typeMap[DafnyTokenKind.VariableIdentifierDefinition] = typeService.GetClassificationType("Dafny identifier");

 

       if (!DafnyMenuWasInitialized)

       {

@@ -119,4 +126,7 @@ namespace DafnyLanguage
     [Name("Dafny identifier")]

     internal static ClassificationTypeDefinition UserType = null;

   }

+

+  #endregion

+

 }

diff --git a/Source/DafnyExtension/ContentType.cs b/Source/DafnyExtension/ContentType.cs
index d8487f74..950b1e73 100644
--- a/Source/DafnyExtension/ContentType.cs
+++ b/Source/DafnyExtension/ContentType.cs
@@ -1,6 +1,7 @@
 using System.ComponentModel.Composition;

 using Microsoft.VisualStudio.Utilities;

 

+

 namespace DafnyLanguage

 {

   class DafnyContentType

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 4c0ae4fc..9314b294 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -9,6 +9,7 @@ using Dafny = Microsoft.Dafny;
 

 namespace DafnyLanguage

 {

+

   public class DafnyDriver

   {

     readonly string _filename;

@@ -23,10 +24,6 @@ namespace DafnyLanguage
       _filename = filename;

     }

 

-    void RecordError(int line, int col, ErrorCategory cat, string msg) {

-      _errors.Add(new DafnyError(line, col, cat, msg, _snapshot));

-    }

-

     static DafnyDriver() {

       Initialize();

     }

@@ -45,6 +42,8 @@ namespace DafnyLanguage
       }

     }

 

+    #region Parsing and type checking

+

     internal Dafny.Program ProcessResolution() {

       if (!ParseAndTypeCheck()) {

         return null;

@@ -69,6 +68,11 @@ namespace DafnyLanguage
       return true;  // success

     }

 

+    void RecordError(int line, int col, ErrorCategory cat, string msg)

+    {

+      _errors.Add(new DafnyError(line, col, cat, msg, _snapshot));

+    }

+

     class VSErrors : Dafny.Errors

     {

       DafnyDriver dd;

@@ -102,6 +106,20 @@ namespace DafnyLanguage
       }

     }

 

+    #endregion

+

+    #region Compilation

+

+    public static void Compile(Dafny.Program dafnyProgram)

+    {

+      Microsoft.Dafny.DafnyOptions.O.SpillTargetCode = true;

+      Microsoft.Dafny.DafnyDriver.CompileDafnyProgram(dafnyProgram, dafnyProgram.Name);

+    }

+

+    #endregion

+

+    #region Boogie interaction

+

     class DafnyErrorInformationFactory : ErrorInformationFactory

     {

       public override ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId)

@@ -109,7 +127,7 @@ namespace DafnyLanguage
         return new DafnyErrorInformation(tok, msg, requestId);

       }

     }

-    

+

     class DafnyErrorInformation : ErrorInformation

     {

       public DafnyErrorInformation(IToken tok, string msg, string requestId)

@@ -136,24 +154,12 @@ namespace DafnyLanguage
       }

     }

 

-    #region Compilation

-

-    public static void Compile(Dafny.Program dafnyProgram)

-    {

-      Microsoft.Dafny.DafnyOptions.O.SpillTargetCode = true;

-      Microsoft.Dafny.DafnyDriver.CompileDafnyProgram(dafnyProgram, dafnyProgram.Name);

-    }

-

-    #endregion

-

-    #region Boogie interaction

-

-    public static bool Verify(Dafny.Program dafnyProgram, ITextSnapshot snapshot, string requestId, ErrorReporterDelegate er) {

+    public static bool Verify(Dafny.Program dafnyProgram, string requestId, ErrorReporterDelegate er) {

       Dafny.Translator translator = new Dafny.Translator();

       translator.InsertChecksums = true;

       Bpl.Program boogieProgram = translator.Translate(dafnyProgram);

 

-      PipelineOutcome oc = BoogiePipeline(boogieProgram, snapshot, requestId, er);

+      PipelineOutcome oc = BoogiePipeline(boogieProgram, requestId, er);

       switch (oc) {

         case PipelineOutcome.Done:

         case PipelineOutcome.VerificationCompleted:

@@ -171,7 +177,7 @@ namespace DafnyLanguage
     /// else.  Hence, any resolution errors and type checking errors are due to errors in

     /// the translation.

     /// </summary>

-    static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, ITextSnapshot snapshot, string requestId, ErrorReporterDelegate er)

+    static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, string requestId, ErrorReporterDelegate er)

     {

       Contract.Requires(program != null);

 

@@ -212,4 +218,5 @@ namespace DafnyLanguage
 

     #endregion

   }

+

 }

diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index bd1a366f..d76de86d 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.csproj
@@ -69,7 +69,7 @@
     <CopyVsixExtensionFiles>False</CopyVsixExtensionFiles>

     <CopyVsixExtensionLocation>

     </CopyVsixExtensionLocation>

-    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>

+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

     <DebugType>pdbonly</DebugType>

@@ -187,6 +187,7 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="BufferIdleEventUtil.cs" />

+    <Compile Include="GlobalSuppressions.cs" />

     <Compile Include="HoverText.cs" />

     <Compile Include="IdentifierTagger.cs" />

     <Compile Include="ProgressMargin.cs" />

diff --git a/Source/DafnyExtension/ErrorTagger.cs b/Source/DafnyExtension/ErrorTagger.cs
index efd755d8..74765203 100644
--- a/Source/DafnyExtension/ErrorTagger.cs
+++ b/Source/DafnyExtension/ErrorTagger.cs
@@ -1,26 +1,23 @@
 //***************************************************************************

 // Copyright © 2010 Microsoft Corporation.  All Rights Reserved.

-// This code released under the terms of the 

+// 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;

 

+

 namespace DafnyLanguage

 {

+

+  #region Provider

+

   [Export(typeof(ITaggerProvider))]

   [ContentType("dafny")]

   [TagType(typeof(ErrorTag))]

@@ -37,6 +34,11 @@ namespace DafnyLanguage
     }

   }

 

+  #endregion

+

+

+  #region Tagger

+

   /// <summary>

   /// Translate PkgDefTokenTags into ErrorTags and Error List items

   /// </summary>

@@ -82,4 +84,7 @@ namespace DafnyLanguage
       }

     }

   }

+

+  #endregion

+

 }

diff --git a/Source/DafnyExtension/GlobalSuppressions.cs b/Source/DafnyExtension/GlobalSuppressions.cs
new file mode 100644
index 00000000..878ee0c3
--- /dev/null
+++ b/Source/DafnyExtension/GlobalSuppressions.cs
diff --git a/Source/DafnyExtension/HoverText.cs b/Source/DafnyExtension/HoverText.cs
index be806f5b..8f75731a 100644
--- a/Source/DafnyExtension/HoverText.cs
+++ b/Source/DafnyExtension/HoverText.cs
@@ -1,24 +1,22 @@
-using System;

-using System.Collections.Generic;

+using System.Collections.Generic;

+using System.ComponentModel.Composition;

 using System.Linq;

-using System.Text;

-using System.Windows.Input;

 using Microsoft.VisualStudio.Language.Intellisense;

-using System.Collections.ObjectModel;

 using Microsoft.VisualStudio.Text;

 using Microsoft.VisualStudio.Text.Editor;

 using Microsoft.VisualStudio.Text.Tagging;

-using System.ComponentModel.Composition;

 using Microsoft.VisualStudio.Utilities;

-using System.Diagnostics.Contracts;

 

 

 namespace DafnyLanguage

 {

+

+  #region Source Provider

+

   [Export(typeof(IQuickInfoSourceProvider))]

   [ContentType("dafny")]

   [Name("Dafny QuickInfo")]

-  class OokQuickInfoSourceProvider : IQuickInfoSourceProvider

+  class DafnyQuickInfoSourceProvider : IQuickInfoSourceProvider

   {

     [Import]

     IBufferTagAggregatorFactoryService aggService = null;

@@ -33,31 +31,40 @@ namespace DafnyLanguage
     private ITagAggregator<DafnyTokenTag> _aggregator;

     private ITextBuffer _buffer;

 

-    public DafnyQuickInfoSource(ITextBuffer buffer, ITagAggregator<DafnyTokenTag> aggregator) {

+    public DafnyQuickInfoSource(ITextBuffer buffer, ITagAggregator<DafnyTokenTag> aggregator)

+    {

       _aggregator = aggregator;

       _buffer = buffer;

     }

 

-    public void AugmentQuickInfoSession(IQuickInfoSession session, IList<object> quickInfoContent, out ITrackingSpan applicableToSpan) {

+    public void AugmentQuickInfoSession(IQuickInfoSession session, IList<object> quickInfoContent, out ITrackingSpan applicableToSpan)

+    {

       applicableToSpan = null;

 

       var triggerPoint = (SnapshotPoint)session.GetTriggerPoint(_buffer.CurrentSnapshot);

       if (triggerPoint == null)

         return;

 

-      foreach (IMappingTagSpan<DafnyTokenTag> curTag in _aggregator.GetTags(new SnapshotSpan(triggerPoint, triggerPoint))) {

+      foreach (IMappingTagSpan<DafnyTokenTag> curTag in _aggregator.GetTags(new SnapshotSpan(triggerPoint, triggerPoint)))

+      {

         var s = curTag.Tag.HoverText;

-        if (s != null) {

+        if (s != null)

+        {

           var tagSpan = curTag.Span.GetSpans(_buffer).First();

           applicableToSpan = _buffer.CurrentSnapshot.CreateTrackingSpan(tagSpan, SpanTrackingMode.EdgeExclusive);

           quickInfoContent.Add(s);

         }

       }

     }

-    public void Dispose() {

+    public void Dispose()

+    {

     }

   }

-  // --------------------------------- QuickInfo controller ------------------------------------------

+

+  #endregion

+

+

+  #region Controller Provider

 

   [Export(typeof(IIntellisenseControllerProvider))]

   [Name("Dafny QuickInfo controller")]

@@ -72,6 +79,11 @@ namespace DafnyLanguage
     }

   }

 

+  #endregion

+

+

+  #region Controller

+

   class DafnyQuickInfoController : IIntellisenseController

   {

     private ITextView _textView;

@@ -123,4 +135,7 @@ namespace DafnyLanguage
         PositionAffinity.Predecessor);

     }

   }

+

+  #endregion

+

 }

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index a4cd3547..86fb2696 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -1,29 +1,26 @@
 //***************************************************************************

 // Copyright © 2010 Microsoft Corporation.  All Rights Reserved.

-// This code released under the terms of the 

+// 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 System.Diagnostics.Contracts;

+using Microsoft.Dafny;

 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 System.Diagnostics.Contracts;

 using Bpl = Microsoft.Boogie;

-using Microsoft.Dafny;

+

 

 namespace DafnyLanguage

 {

+

+  #region Provider

+

   [Export(typeof(ITaggerProvider))]

   [ContentType("dafny")]

   [TagType(typeof(DafnyTokenTag))]

@@ -40,6 +37,11 @@ namespace DafnyLanguage
     }

   }

 

+  #endregion

+

+

+  #region Tagger

+

   /// <summary>

   /// Translate DafnyResolverTag's into IOutliningRegionTag's

   /// </summary>

@@ -77,14 +79,14 @@ namespace DafnyLanguage
       int end = entire.End;

       foreach (var r in _regions) {

         if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) {

-          DafnyTokenKinds kind;

+          DafnyTokenKind kind;

           switch (r.Kind) {

             case IdRegion.OccurrenceKind.Use:

-              kind = DafnyTokenKinds.VariableIdentifier; break;

+              kind = DafnyTokenKind.VariableIdentifier; break;

             case IdRegion.OccurrenceKind.Definition:

-              kind = DafnyTokenKinds.VariableIdentifierDefinition; break;

+              kind = DafnyTokenKind.VariableIdentifierDefinition; break;

             case IdRegion.OccurrenceKind.WildDefinition:

-              kind = DafnyTokenKinds.Keyword; break;

+              kind = DafnyTokenKind.Keyword; break;

             default:

               Contract.Assert(false);  // unexpected OccurrenceKind

               goto case IdRegion.OccurrenceKind.Use;  // to please compiler

@@ -386,4 +388,6 @@ namespace DafnyLanguage
     }

   }

 

+  #endregion

+

 }

diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs
index 2c5a7fbd..0e7d1f1d 100644
--- a/Source/DafnyExtension/OutliningTagger.cs
+++ b/Source/DafnyExtension/OutliningTagger.cs
@@ -1,29 +1,26 @@
 //***************************************************************************

 // Copyright © 2010 Microsoft Corporation.  All Rights Reserved.

-// This code released under the terms of the 

+// 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 System.Diagnostics.Contracts;

 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 System.Diagnostics.Contracts;

 using Bpl = Microsoft.Boogie;

 using Dafny = Microsoft.Dafny;

 

+

 namespace DafnyLanguage

 {

+

+  #region Provider

+

   [Export(typeof(ITaggerProvider))]

   [ContentType("dafny")]

   [TagType(typeof(IOutliningRegionTag))]

@@ -40,6 +37,11 @@ namespace DafnyLanguage
     }

   }

 

+  #endregion

+

+

+  #region Tagger

+

   /// <summary>

   /// Translate DafnyResolverTag's into IOutliningRegionTag's

   /// </summary>

@@ -48,7 +50,7 @@ namespace DafnyLanguage
     ITextBuffer _buffer;

     ITextSnapshot _snapshot;  // the most recent snapshot of _buffer that we have been informed about

     Dafny.Program _program;  // the program parsed from _snapshot

-    List<ORegion> _regions = new List<ORegion>();  // the regions generated from _program

+    List<OutliningRegion> _regions = new List<OutliningRegion>();  // the regions generated from _program

     ITagAggregator<DafnyResolverTag> _aggregator;

 

     internal OutliningTagger(ITextBuffer buffer, ITagAggregator<DafnyResolverTag> tagAggregator) {

@@ -120,7 +122,7 @@ namespace DafnyLanguage
       if (program == _program)

         return false;  // no new regions

 

-      List<ORegion> newRegions = new List<ORegion>();

+      List<OutliningRegion> newRegions = new List<OutliningRegion>();

 

       foreach (var module in program.Modules) {

         if (!module.IsDefaultModule) {

@@ -128,18 +130,18 @@ namespace DafnyLanguage
           if (module.IsAbstract) {

             nm = "abstract " + nm;

           }

-          newRegions.Add(new ORegion(module, nm));

+          newRegions.Add(new OutliningRegion(module, nm));

         }

         foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) {

           if (!HasBodyTokens(d) && !(d is Dafny.ClassDecl)) {

             continue;

           }

           if (d is Dafny.ArbitraryTypeDecl) {

-            newRegions.Add(new ORegion(d, "type"));

+            newRegions.Add(new OutliningRegion(d, "type"));

           } else if (d is Dafny.CoDatatypeDecl) {

-            newRegions.Add(new ORegion(d, "codatatype"));

+            newRegions.Add(new OutliningRegion(d, "codatatype"));

           } else if (d is Dafny.DatatypeDecl) {

-            newRegions.Add(new ORegion(d, "datatype"));

+            newRegions.Add(new OutliningRegion(d, "datatype"));

           } else if (d is Dafny.ModuleDecl) {

             // do nothing here, since the outer loop handles modules

           } else {

@@ -147,9 +149,9 @@ namespace DafnyLanguage
             if (cl.IsDefaultClass) {

               // do nothing

             } else if (cl is Dafny.IteratorDecl) {

-              newRegions.Add(new ORegion(cl, "iterator"));

+              newRegions.Add(new OutliningRegion(cl, "iterator"));

             } else {

-              newRegions.Add(new ORegion(cl, "class"));

+              newRegions.Add(new OutliningRegion(cl, "class"));

             }

             // do the class members (in particular, functions and methods)

             foreach (Dafny.MemberDecl m in cl.Members) {

@@ -165,7 +167,7 @@ namespace DafnyLanguage
                 if (!m.IsGhost) {

                   nm += " method";

                 }

-                newRegions.Add(new ORegion(m, nm));

+                newRegions.Add(new OutliningRegion(m, nm));

               } else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) {

                 var nm =

                   m is Dafny.Constructor ? "constructor" :

@@ -175,7 +177,7 @@ namespace DafnyLanguage
                 if (m.IsGhost && !(m is Dafny.CoMethod)) {

                   nm = "ghost " + nm;

                 }

-                newRegions.Add(new ORegion(m, nm));

+                newRegions.Add(new OutliningRegion(m, nm));

               }

             }

           }

@@ -187,17 +189,17 @@ namespace DafnyLanguage
       return true;

     }

 

-    bool HasBodyTokens(Dafny.Declaration decl) {

+    static bool HasBodyTokens(Dafny.Declaration decl) {

       Contract.Requires(decl != null);

       return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken;

     }

 

-    class ORegion

+    class OutliningRegion

     {

       public readonly int Start;

       public readonly int Length;

       public readonly string HoverText;

-      public ORegion(Dafny.Declaration decl, string kind) {

+      public OutliningRegion(Dafny.Declaration decl, string kind) {

         int startPosition = decl.BodyStartTok.pos + 1;  // skip the open-curly brace itself

         int length = decl.BodyEndTok.pos - startPosition;

         Start = startPosition;

@@ -206,4 +208,7 @@ namespace DafnyLanguage
       }

     }

   }

+

+  #endregion

+

 }

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index 7a6669ae..b964776d 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -21,6 +21,7 @@ using Dafny = Microsoft.Dafny;
 

 namespace DafnyLanguage

 {

+

   #region UI stuff

   internal class ProgressMarginGlyphFactory : IGlyphFactory

   {

@@ -60,6 +61,9 @@ namespace DafnyLanguage
   }

   #endregion

 

+

+  #region Provider

+

   [Export(typeof(ITaggerProvider))]

   [ContentType("dafny")]

   [TagType(typeof(ProgressGlyphTag))]

@@ -82,6 +86,11 @@ namespace DafnyLanguage
     }

   }

 

+  #endregion

+

+

+  #region Tagger

+

   public class ProgressTagger : ITagger<ProgressGlyphTag>, IDisposable

   {

     ErrorListProvider _errorProvider;

@@ -170,7 +179,7 @@ namespace DafnyLanguage
       get { return verificationDisabled; }

     }

 

-    public static IDictionary<string, ProgressTagger> ProgressTaggers = new ConcurrentDictionary<string, ProgressTagger>();

+    public static readonly IDictionary<string, ProgressTagger> ProgressTaggers = new ConcurrentDictionary<string, ProgressTagger>();

 

     public readonly ConcurrentDictionary<string, ITextSnapshot> RequestIdToSnapshot = new ConcurrentDictionary<string, ITextSnapshot>();

 

@@ -287,7 +296,7 @@ namespace DafnyLanguage
       // Run the verifier

       var newErrors = new List<DafnyError>();

       try {

-        bool success = DafnyDriver.Verify(program, snapshot, requestId, errorInfo =>

+        bool success = DafnyDriver.Verify(program, requestId, errorInfo =>

         {

           ITextSnapshot s = snapshot;

           if (errorInfo.RequestId != null)

@@ -309,7 +318,7 @@ namespace DafnyLanguage
 

       errorListHolder.VerificationErrors = newErrors;

       errorListHolder.UpdateErrorList(snapshot);

-      

+

       lock (this) {

         bufferChangesPreVerificationStart.Clear();

         verificationInProgress = false;

@@ -336,7 +345,7 @@ namespace DafnyLanguage
       }

 

       // If the requested snapshot isn't the same as the one our words are on, translate our spans to the expected snapshot

-      var chs = new NormalizedSnapshotSpanCollection(pre.Select(span => span.TranslateTo(targetSnapshot, SpanTrackingMode.EdgeExclusive)));      

+      var chs = new NormalizedSnapshotSpanCollection(pre.Select(span => span.TranslateTo(targetSnapshot, SpanTrackingMode.EdgeExclusive)));

       foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, chs)) {

         yield return new TagSpan<ProgressGlyphTag>(span, new ProgressGlyphTag(0));

       }

@@ -346,4 +355,7 @@ namespace DafnyLanguage
       }

     }

   }

+

+  #endregion

+

 }

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index a4d4a690..349bc09f 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -1,15 +1,16 @@
 //***************************************************************************

 // Copyright © 2010 Microsoft Corporation.  All Rights Reserved.

-// This code released under the terms of the 

+// This code released under the terms of the

 // Microsoft Public License (MS-PL, http://opensource.org/licenses/ms-pl.html.)

 //***************************************************************************

 

+

 using System;

-using System.Linq;

 using System.Collections.Concurrent;

 using System.Collections.Generic;

 using System.ComponentModel.Composition;

 using System.Diagnostics.Contracts;

+using System.Linq;

 using EnvDTE;

 using Microsoft.VisualStudio;

 using Microsoft.VisualStudio.Shell;

@@ -20,8 +21,12 @@ using Microsoft.VisualStudio.TextManager.Interop;
 using Microsoft.VisualStudio.Utilities;

 using Dafny = Microsoft.Dafny;

 

+

 namespace DafnyLanguage

 {

+

+  #region Provider

+

   [Export(typeof(ITaggerProvider))]

   [ContentType("dafny")]

   [TagType(typeof(DafnyResolverTag))]

@@ -40,9 +45,17 @@ namespace DafnyLanguage
     }

   }

 

+  #endregion

+

+

+  #region Tagger

+

+  #region Tags

+

   public abstract class DafnyResolverTag : ITag

   {

   }

+

   public class DafnyErrorResolverTag : DafnyResolverTag

   {

     public readonly string Typ;

@@ -52,6 +65,7 @@ namespace DafnyLanguage
       Msg = msg;

     }

   }

+

   public class DafnySuccessResolverTag : DafnyResolverTag

   {

     public readonly Dafny.Program Program;

@@ -60,6 +74,9 @@ namespace DafnyLanguage
     }

   }

 

+  #endregion

+

+

   /// <summary>

   /// Translate PkgDefTokenTags into ErrorTags and Error List items

   /// </summary>

@@ -74,7 +91,7 @@ namespace DafnyLanguage
     public Dafny.Program _program;  // non-null only if the snapshot contains a Dafny program that type checks

 

     List<DafnyError> _resolutionErrors = new List<DafnyError>();  // if nonempty, then _snapshot is the snapshot from which the errors were produced

-    

+

     List<DafnyError> _verificationErrors = new List<DafnyError>();

     public List<DafnyError> VerificationErrors

     {

@@ -259,7 +276,7 @@ namespace DafnyLanguage
         chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));

     }

 

-    TaskErrorCategory CategoryConversion(ErrorCategory cat) {

+    static TaskErrorCategory CategoryConversion(ErrorCategory cat) {

       switch (cat) {

         case ErrorCategory.ParseError:

         case ErrorCategory.ResolveError:

@@ -325,6 +342,9 @@ namespace DafnyLanguage
 

   }

 

+

+  #region Errors

+

   public enum ErrorCategory

   {

     ProcessError, ParseWarning, ParseError, ResolveError, VerificationError, AuxInformation, InternalError

@@ -355,4 +375,9 @@ namespace DafnyLanguage
       Span = new SnapshotSpan(sLine.Start + Column, sLength);

     }

   }

+

+  #endregion

+

+  #endregion

+

 }

diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index e430f60f..4980bf0a 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -1,16 +1,17 @@
 using System;

 using System.Collections.Generic;

-using System.Linq;

 using System.ComponentModel.Composition;

+using System.Linq;

 using Microsoft.VisualStudio.Text;

-using Microsoft.VisualStudio.Text.Classification;

-using Microsoft.VisualStudio.Text.Editor;

 using Microsoft.VisualStudio.Text.Tagging;

 using Microsoft.VisualStudio.Utilities;

-using Dafny = Microsoft.Dafny;

+

 

 namespace DafnyLanguage

 {

+

+  #region Provider

+

   [Export(typeof(ITaggerProvider))]

   [ContentType("dafny")]

   [TagType(typeof(DafnyTokenTag))]

@@ -21,7 +22,12 @@ namespace DafnyLanguage
     }

   }

 

-  public enum DafnyTokenKinds

+  #endregion

+

+

+  #region Tagger

+

+  public enum DafnyTokenKind

   {

     Keyword, Number, String, Comment,

     VariableIdentifier, VariableIdentifierDefinition

@@ -29,14 +35,14 @@ namespace DafnyLanguage
 

   public class DafnyTokenTag : ITag

   {

-    public DafnyTokenKinds Kind { get; private set; }

+    public DafnyTokenKind Kind { get; private set; }

     public string HoverText { get; private set; }

 

-    public DafnyTokenTag(DafnyTokenKinds kind) {

+    public DafnyTokenTag(DafnyTokenKind kind) {

       this.Kind = kind;

     }

 

-    public DafnyTokenTag(DafnyTokenKinds kind, string hoverText) {

+    public DafnyTokenTag(DafnyTokenKind kind, string hoverText) {

       this.Kind = kind;

       this.HoverText = hoverText;

     }

@@ -46,7 +52,7 @@ namespace DafnyLanguage
   {

     ITextBuffer _buffer;

     ITextSnapshot _snapshot;

-    List<DRegion> _regions;

+    List<TokenRegion> _regions;

 

     internal DafnyTokenTagger(ITextBuffer buffer) {

       _buffer = buffer;

@@ -57,17 +63,17 @@ namespace DafnyLanguage
     }

 

     public event EventHandler<SnapshotSpanEventArgs> TagsChanged;

-    

+

     public IEnumerable<ITagSpan<DafnyTokenTag>> GetTags(NormalizedSnapshotSpanCollection spans) {

       if (spans.Count == 0)

         yield break;

 

-      List<DRegion> currentRegions = _regions;

+      List<TokenRegion> currentRegions = _regions;

       ITextSnapshot currentSnapshot = _snapshot;

 

       // create a new SnapshotSpan for the entire region encompassed by the span collection

       SnapshotSpan entire = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End).TranslateTo(currentSnapshot, SpanTrackingMode.EdgeExclusive);

-      

+

       // return tags for any regions that fall within that span

       // BUGBUG: depending on how GetTags gets called (e.g., once for each line in the buffer), this may produce quadratic behavior

       foreach (var region in currentRegions) {

@@ -85,9 +91,9 @@ namespace DafnyLanguage
       ITextSnapshot snapshot = _buffer.CurrentSnapshot;

       if (snapshot == _snapshot)

         return;  // we've already computed the regions for this snapshot

-       

+

       // get all of the outline regions in the snapshot

-      List<DRegion> newRegions = Rescan(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 =>

@@ -112,26 +118,26 @@ namespace DafnyLanguage
       }

     }

 

-    NormalizedSnapshotSpanCollection SymmetricDifference(NormalizedSnapshotSpanCollection first, NormalizedSnapshotSpanCollection second) {

+    static NormalizedSnapshotSpanCollection SymmetricDifference(NormalizedSnapshotSpanCollection first, NormalizedSnapshotSpanCollection second) {

       return NormalizedSnapshotSpanCollection.Union(

           NormalizedSnapshotSpanCollection.Difference(first, second),

           NormalizedSnapshotSpanCollection.Difference(second, first));

     }

 

-    private static List<DRegion> Rescan(ITextSnapshot newSnapshot) {

-      List<DRegion> newRegions = new List<DRegion>();

+    private static List<TokenRegion> Rescan(ITextSnapshot newSnapshot) {

+      List<TokenRegion> newRegions = new List<TokenRegion>();

 

       bool stillScanningLongComment = false;

       SnapshotPoint commentStart = new SnapshotPoint();  // used only when stillScanningLongComment

       SnapshotPoint commentEndAsWeKnowIt = new SnapshotPoint();  // used only when stillScanningLongComment

       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 N = txt.Length;  // length of the current line

         int cur = 0;  // offset into the current line

 

         if (stillScanningLongComment) {

           if (ScanForEndOfComment(txt, ref cur)) {

-            newRegions.Add(new DRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + cur), DafnyTokenKinds.Comment));

+            newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + cur), DafnyTokenKind.Comment));

             stillScanningLongComment = false;

           } else {

             commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + cur);

@@ -142,7 +148,7 @@ namespace DafnyLanguage
         int end;  // offset into the current line

         for (; ; cur = end) {

           // advance to the first character of a keyword or token

-          DafnyTokenKinds ty = DafnyTokenKinds.Keyword;

+          DafnyTokenKind ty = DafnyTokenKind.Keyword;

           for (; ; cur++) {

             if (N <= cur) {

               // we've looked at everything in this line

@@ -151,22 +157,22 @@ namespace DafnyLanguage
             char ch = txt[cur];

             if ('a' <= ch && ch <= 'z') break;

             if ('A' <= ch && ch <= 'Z') break;

-            if ('0' <= ch && ch <= '9') { ty = DafnyTokenKinds.Number; break; }

-            if (ch == '"') { ty = DafnyTokenKinds.String; break; }

-            if (ch == '/') { ty = DafnyTokenKinds.Comment; break; }

+            if ('0' <= ch && ch <= '9') { ty = DafnyTokenKind.Number; break; }

+            if (ch == '"') { ty = DafnyTokenKind.String; break; }

+            if (ch == '/') { ty = DafnyTokenKind.Comment; break; }

             if (ch == '\'' || ch == '_' || ch == '?' || ch == '\\') break;  // parts of identifiers

           }

 

           // advance to the end of the token

           end = cur + 1;  // offset into the current line

-          if (ty == DafnyTokenKinds.Number) {

+          if (ty == DafnyTokenKind.Number) {

             // scan the rest of this number

             for (; end < N; end++) {

               char ch = txt[end];

               if ('0' <= ch && ch <= '9') {

               } else break;

             }

-          } else if (ty == DafnyTokenKinds.String) {

+          } else if (ty == DafnyTokenKind.String) {

             // scan the rest of this string, but not past the end-of-line

             for (; end < N; end++) {

               char ch = txt[end];

@@ -183,7 +189,7 @@ namespace DafnyLanguage
                 }

               }

             }

-          } else if (ty == DafnyTokenKinds.Comment) {

+          } else if (ty == DafnyTokenKind.Comment) {

             if (end == N) continue;  // this was not the start of a comment

             char ch = txt[end];

             if (ch == '/') {

@@ -194,7 +200,7 @@ namespace DafnyLanguage
               end++;

               commentStart = new SnapshotPoint(newSnapshot, line.Start + cur);

               if (ScanForEndOfComment(txt, ref end)) {

-                newRegions.Add(new DRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + end), DafnyTokenKinds.Comment));

+                newRegions.Add(new TokenRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + end), DafnyTokenKind.Comment));

               } else {

                 stillScanningLongComment = true;

                 commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + end);

@@ -297,13 +303,13 @@ namespace DafnyLanguage
             }

           }

 

-          newRegions.Add(new DRegion(new SnapshotPoint(newSnapshot, line.Start + cur), new SnapshotPoint(newSnapshot, line.Start + end), ty));

+          newRegions.Add(new TokenRegion(new SnapshotPoint(newSnapshot, line.Start + cur), new SnapshotPoint(newSnapshot, line.Start + end), ty));

         }

       OUTER_CONTINUE: ;

       }

 

       if (stillScanningLongComment) {

-        newRegions.Add(new DRegion(commentStart, commentEndAsWeKnowIt, DafnyTokenKinds.Comment));

+        newRegions.Add(new TokenRegion(commentStart, commentEndAsWeKnowIt, DafnyTokenKind.Comment));

       }

 

       return newRegions;

@@ -325,19 +331,22 @@ namespace DafnyLanguage
     }

   }

 

-  internal class DRegion

+  internal class TokenRegion

   {

     public SnapshotPoint Start { get; private set; }

     public SnapshotPoint End { get; private set; }

     public SnapshotSpan Span {

       get { return new SnapshotSpan(Start, End); }

     }

-    public DafnyTokenKinds Kind { get; private set; }

+    public DafnyTokenKind Kind { get; private set; }

 

-    public DRegion(SnapshotPoint start, SnapshotPoint end, DafnyTokenKinds kind) {

+    public TokenRegion(SnapshotPoint start, SnapshotPoint end, DafnyTokenKind kind) {

       Start = start;

       End = end;

       Kind = kind;

     }

   }

+

+  #endregion

+

 }

diff --git a/Source/DafnyExtension/WordHighlighter.cs b/Source/DafnyExtension/WordHighlighter.cs
index 03456c85..4c0fbb28 100644
--- a/Source/DafnyExtension/WordHighlighter.cs
+++ b/Source/DafnyExtension/WordHighlighter.cs
@@ -2,7 +2,6 @@
 using System.Collections.Generic;

 using System.ComponentModel.Composition;

 using System.Linq;

-using System.Threading;

 using System.Windows.Media;

 using Microsoft.VisualStudio.Text;

 using Microsoft.VisualStudio.Text.Classification;

@@ -11,10 +10,14 @@ using Microsoft.VisualStudio.Text.Operations;
 using Microsoft.VisualStudio.Text.Tagging;

 using Microsoft.VisualStudio.Utilities;

 

+

 namespace DafnyLanguage

 {

+

 #if LATER_MAYBE

-  #region // (the current annoying) word highligher

+

+  #region (the current annoying) word highligher

+

   internal class HighlightWordTagger : ITagger<HighlightWordTag>

   {

     ITextView View { get; set; }

@@ -82,7 +85,7 @@ namespace DafnyLanguage
              || char.IsWhiteSpace((currentRequest - 1).GetChar())) {

           foundWord = false;

         } else {

-          // Try again, one character previous. 

+          // Try again, one character previous.

           //If the caret is at the end of a word, pick up the word.

           word = TextStructureNavigator.GetExtentOfWord(currentRequest - 1);

 

@@ -206,6 +209,9 @@ namespace DafnyLanguage
       return new HighlightWordTagger(textView, buffer, TextSearchService, textStructureNavigator) as ITagger<T>;

     }

   }

-#endregion

+

+  #endregion

+

 #endif

+

 }

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index dcd4344e..54f3a4dd 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -17,8 +17,8 @@ namespace DafnyLanguage.DafnyMenu
   /// The minimum requirement for a class to be considered a valid package for Visual Studio

   /// is to implement the IVsPackage interface and register itself with the shell.

   /// This package uses the helper classes defined inside the Managed Package Framework (MPF)

-  /// to do it: it derives from the Package class that provides the implementation of the 

-  /// IVsPackage interface and uses the registration attributes defined in the framework to 

+  /// to do it: it derives from the Package class that provides the implementation of the

+  /// IVsPackage interface and uses the registration attributes defined in the framework to

   /// register itself and its components with the shell.

   /// </summary>

   // This attribute tells the PkgDef creation utility (CreatePkgDef.exe) that this class is

@@ -41,9 +41,9 @@ namespace DafnyLanguage.DafnyMenu
 

     /// <summary>

     /// Default constructor of the package.

-    /// Inside this method you can place any initialization code that does not require 

-    /// any Visual Studio service because at this point the package object is created but 

-    /// not sited yet inside Visual Studio environment. The place to do all the other 

+    /// Inside this method you can place any initialization code that does not require

+    /// any Visual Studio service because at this point the package object is created but

+    /// not sited yet inside Visual Studio environment. The place to do all the other

     /// initialization is the Initialize method.

     /// </summary>

     public DafnyMenuPackage()

@@ -128,7 +128,7 @@ namespace DafnyLanguage.DafnyMenu
     {

       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

       DafnyLanguage.ProgressTagger tagger;

-      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);  

+      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);

       runVerifierCommand.Visible = tagger != null && tagger.VerificationDisabled;

       runVerifierCommand.Enabled = tagger != null && tagger.VerificationDisabled;

     }

@@ -137,7 +137,7 @@ namespace DafnyLanguage.DafnyMenu
     {

       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

       DafnyLanguage.ProgressTagger tagger;

-      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);  

+      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);

       stopVerifierCommand.Visible = !(tagger != null && tagger.VerificationDisabled);

       stopVerifierCommand.Enabled = !(tagger != null && tagger.VerificationDisabled);

     }