visual studio extension

2017-03-26 20:31:23 -07:00 · 2017-03-26 20:31:23 -07:00 · 918f5b3914
--- a/vs/ext/BraceMatching.cs
+++ b/vs/ext/BraceMatching.cs
@ -0,0 +1,265 @@
+using System;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+
+
+namespace IvyLanguage
+{
+
+  #region Provider
+
+  [Export(typeof(IViewTaggerProvider))]
+  [ContentType("ivy")]
+  [TagType(typeof(TextMarkerTag))]
+  internal class BraceMatchingTaggerProvider : IViewTaggerProvider
+  {
+    [Import]
+    internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
+
+    public ITagger<T> CreateTagger<T>(ITextView textView, ITextBuffer buffer) where T : ITag {
+      if (textView == null)
+        return null;
+
+      //provide highlighting only on the top-level buffer
+      if (textView.TextBuffer != buffer)
+        return null;
+
+      ITagAggregator<IvyTokenTag> tagAggregator = AggregatorFactory.CreateTagAggregator<IvyTokenTag>(buffer);
+      return new BraceMatchingTagger(textView, buffer, tagAggregator) as ITagger<T>;
+    }
+  }
+
+  #endregion
+
+
+  #region Tagger
+
+  internal abstract class TokenBasedTagger
+  {
+    ITagAggregator<IvyTokenTag> _aggregator;
+
+    internal TokenBasedTagger(ITagAggregator<IvyTokenTag> tagAggregator) {
+      _aggregator = tagAggregator;
+    }
+
+    public bool InsideComment(SnapshotPoint pt) {
+      SnapshotSpan span = new SnapshotSpan(pt, 1);
+      foreach (var tagSpan in this._aggregator.GetTags(span)) {
+        switch (tagSpan.Tag.Kind) {
+          case IvyTokenKind.Comment:
+          case IvyTokenKind.String:
+            foreach (var s in tagSpan.Span.GetSpans(pt.Snapshot)) {
+              if (s.Contains(span))
+                return true;
+            }
+            break;
+          default:
+            break;
+        }
+      }
+      return false;
+    }
+  }
+
+
+  internal class BraceMatchingTagger : TokenBasedTagger, ITagger<TextMarkerTag>
+  {
+    ITextView View { get; set; }
+    ITextBuffer SourceBuffer { get; set; }
+    SnapshotPoint? CurrentChar { get; set; }
+    private char[] openBraces;
+    private char[] closeBraces;
+
+    static TextMarkerTag Blue = new TextMarkerTag("blue");
+
+    internal BraceMatchingTagger(ITextView view, ITextBuffer sourceBuffer, ITagAggregator<IvyTokenTag> tagAggregator)
+      : base(tagAggregator)
+    {
+      //here the keys are the open braces, and the values are the close braces
+      openBraces =  new char[] { '(', '{', '[' };
+      closeBraces = new char[] { ')', '}', ']' };
+      this.View = view;
+      this.SourceBuffer = sourceBuffer;
+      this.CurrentChar = null;
+
+      this.View.Caret.PositionChanged += CaretPositionChanged;
+      this.View.LayoutChanged += ViewLayoutChanged;
+    }
+
+    public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+    void ViewLayoutChanged(object sender, TextViewLayoutChangedEventArgs e) {
+      if (e.NewSnapshot != e.OldSnapshot) //make sure that there has really been a change
+      {
+        UpdateAtCaretPosition(View.Caret.Position);
+      }
+    }
+
+    void CaretPositionChanged(object sender, CaretPositionChangedEventArgs e) {
+      UpdateAtCaretPosition(e.NewPosition);
+    }
+
+    void UpdateAtCaretPosition(CaretPosition caretPosition) {
+      CurrentChar = caretPosition.Point.GetPoint(SourceBuffer, caretPosition.Affinity);
+
+      if (!CurrentChar.HasValue)
+        return;
+
+      var chngd = TagsChanged;
+      if (chngd != null)
+        chngd(this, new SnapshotSpanEventArgs(new SnapshotSpan(SourceBuffer.CurrentSnapshot, 0, SourceBuffer.CurrentSnapshot.Length)));
+    }
+
+    public IEnumerable<ITagSpan<TextMarkerTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+      if (spans.Count == 0)   //there is no content in the buffer
+        yield break;
+
+      //don't do anything if the current SnapshotPoint is not initialized
+      if (!CurrentChar.HasValue)
+        yield break;
+
+      //hold on to a snapshot of the current character
+      SnapshotPoint currentChar = CurrentChar.Value;
+
+      //if the requested snapshot isn't the same as the one the brace is on, translate our spans to the expected snapshot
+      if (spans[0].Snapshot != currentChar.Snapshot) {
+        currentChar = currentChar.TranslateTo(spans[0].Snapshot, PointTrackingMode.Positive);
+      }
+
+      if (currentChar.Position < spans[0].Snapshot.Length) {
+        // Check if the current character is an open brace
+        char ch = currentChar.GetChar();
+        char closeCh;
+        if (MatchBrace(currentChar, ch, true, out closeCh)) {
+          SnapshotSpan pairSpan;
+          if (FindMatchingCloseChar(currentChar, ch, closeCh, View.TextViewLines.Count, out pairSpan)) {
+            yield return new TagSpan<TextMarkerTag>(new SnapshotSpan(currentChar, 1), Blue);
+            yield return new TagSpan<TextMarkerTag>(pairSpan, Blue);
+          }
+        }
+      }
+
+      if (0 < currentChar.Position) {
+        // Check if the previous character is a close brace (note, caret may be between a close brace and an open brace, in which case we'll tag two pairs)
+        SnapshotPoint prevChar = currentChar - 1;
+        char ch = prevChar.GetChar();
+        char openCh;
+        if (MatchBrace(prevChar, ch, false, out openCh)) {
+          SnapshotSpan pairSpan;
+          if (FindMatchingOpenChar(prevChar, openCh, ch, View.TextViewLines.Count, out pairSpan)) {
+            yield return new TagSpan<TextMarkerTag>(new SnapshotSpan(prevChar, 1), Blue);
+            yield return new TagSpan<TextMarkerTag>(pairSpan, Blue);
+          }
+        }
+      }
+    }
+
+    private bool MatchBrace(SnapshotPoint pt, char query, bool sourceIsOpen, out char match) {
+      if (!InsideComment(pt)) {
+        char[] source = sourceIsOpen ? openBraces : closeBraces;
+        int i = 0;
+        foreach (char ch in source) {
+          if (ch == query) {
+            char[] dest = sourceIsOpen ? closeBraces : openBraces;
+            match = dest[i];
+            return true;
+          }
+          i++;
+        }
+      }
+      match = query;  // satisfy compiler
+      return false;
+    }
+
+    private bool FindMatchingCloseChar(SnapshotPoint startPoint, char open, char close, int linesViewed, out SnapshotSpan pairSpan) {
+      ITextSnapshotLine line = startPoint.GetContainingLine();
+      int lineNumber = line.LineNumber;
+      int offset = startPoint.Position - line.Start.Position + 1;
+
+      int lineNumberLimit = Math.Min(startPoint.Snapshot.LineCount, lineNumber + linesViewed);
+
+      int openCount = 0;
+      while (true) {
+        string lineText = line.GetText();
+
+        //walk the entire line
+        for (; offset < line.Length; offset++) {
+          char currentChar = lineText[offset];
+          if (currentChar == open || currentChar == close) {
+            if (!InsideComment(new SnapshotPoint(line.Snapshot, line.Start.Position + offset))) {
+              if (currentChar == open) {
+                openCount++;
+              } else if (0 < openCount) {
+                openCount--;
+              } else {
+                //found the matching close
+                pairSpan = new SnapshotSpan(startPoint.Snapshot, line.Start + offset, 1);
+                return true;
+              }
+            }
+          }
+        }
+
+        //move on to the next line
+        lineNumber++;
+        if (lineNumberLimit <= lineNumber)
+          break;
+
+        line = line.Snapshot.GetLineFromLineNumber(lineNumber);
+        offset = 0;
+      }
+
+      pairSpan = new SnapshotSpan(startPoint, startPoint);  // satisfy the compiler
+      return false;
+    }
+
+    private bool FindMatchingOpenChar(SnapshotPoint startPoint, char open, char close, int linesViewed, out SnapshotSpan pairSpan) {
+      ITextSnapshotLine line = startPoint.GetContainingLine();
+      int lineNumber = line.LineNumber;
+      int offset = startPoint.Position - line.Start.Position - 1; //move the offset to the character before this one
+
+      int lineNumberLimit = Math.Max(0, lineNumber - linesViewed);
+
+      int closeCount = 0;
+      while (true) {
+        string lineText = line.GetText();
+
+        //walk the entire line
+        for (; 0 <= offset; offset--) {
+          char currentChar = lineText[offset];
+          if (currentChar == open || currentChar == close) {
+            if (!InsideComment(new SnapshotPoint(line.Snapshot, line.Start.Position + offset))) {
+              if (currentChar == close) {
+                closeCount++;
+              } else if (0 < closeCount) {
+                closeCount--;
+              } else {
+                // We've found the open character
+                pairSpan = new SnapshotSpan(line.Start + offset, 1); //we just want the character itself
+                return true;
+              }
+            }
+          }
+        }
+
+        // Move to the previous line
+        lineNumber--;
+        if (lineNumber < lineNumberLimit)
+          break;
+
+        line = line.Snapshot.GetLineFromLineNumber(lineNumber);
+        offset = line.Length - 1;
+      }
+
+      pairSpan = new SnapshotSpan(startPoint, startPoint);  // satisfy the compiler
+      return false;
+    }
+  }
+
+  #endregion
+
+}
--- a/vs/ext/BufferIdleEventUtil.cs
+++ b/vs/ext/BufferIdleEventUtil.cs
@ -0,0 +1,151 @@
+using System;
+using System.Collections.Generic;
+using System.Windows.Threading;
+using Microsoft.VisualStudio.Text;
+
+
+namespace IvyLanguage
+{
+
+    /// <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
+    /// </summary>
+    static class BufferIdleEventUtil
+    {
+        static object bufferListenersKey = new object();
+        static object bufferTimerKey = new object();
+
+        #region Public interface
+
+        public static bool AddBufferIdleEventListener(ITextBuffer buffer, EventHandler handler)
+        {
+            HashSet<EventHandler> listenersForBuffer;
+            if (!TryGetBufferListeners(buffer, out listenersForBuffer))
+                listenersForBuffer = ConnectToBuffer(buffer);
+
+            if (listenersForBuffer.Contains(handler))
+                return false;
+
+            listenersForBuffer.Add(handler);
+
+            return true;
+        }
+
+        public static bool RemoveBufferIdleEventListener(ITextBuffer buffer, EventHandler handler)
+        {
+            HashSet<EventHandler> listenersForBuffer;
+            if (!TryGetBufferListeners(buffer, out listenersForBuffer))
+                return false;
+
+            if (!listenersForBuffer.Contains(handler))
+                return false;
+
+            listenersForBuffer.Remove(handler);
+
+            if (listenersForBuffer.Count == 0)
+                DisconnectFromBuffer(buffer);
+
+            return true;
+        }
+
+        #endregion
+
+        #region Helpers
+
+        static bool TryGetBufferListeners(ITextBuffer buffer, out HashSet<EventHandler> listeners)
+        {
+            return buffer.Properties.TryGetProperty(bufferListenersKey, out listeners);
+        }
+
+        static void ClearBufferListeners(ITextBuffer buffer)
+        {
+            buffer.Properties.RemoveProperty(bufferListenersKey);
+        }
+
+        static bool TryGetBufferTimer(ITextBuffer buffer, out DispatcherTimer timer)
+        {
+            return buffer.Properties.TryGetProperty(bufferTimerKey, out timer);
+        }
+
+        static void ClearBufferTimer(ITextBuffer buffer)
+        {
+            DispatcherTimer timer;
+            if (TryGetBufferTimer(buffer, out timer))
+            {
+                if (timer != null)
+                    timer.Stop();
+                buffer.Properties.RemoveProperty(bufferTimerKey);
+            }
+        }
+
+        static void DisconnectFromBuffer(ITextBuffer buffer)
+        {
+            buffer.Changed -= BufferChanged;
+
+            ClearBufferListeners(buffer);
+            ClearBufferTimer(buffer);
+
+            buffer.Properties.RemoveProperty(bufferListenersKey);
+        }
+
+        static HashSet<EventHandler> ConnectToBuffer(ITextBuffer buffer)
+        {
+            buffer.Changed += BufferChanged;
+
+            RestartTimerForBuffer(buffer);
+
+            HashSet<EventHandler> listenersForBuffer = new HashSet<EventHandler>();
+            buffer.Properties[bufferListenersKey] = listenersForBuffer;
+
+            return listenersForBuffer;
+        }
+
+        static void RestartTimerForBuffer(ITextBuffer buffer)
+        {
+            DispatcherTimer timer;
+
+            if (TryGetBufferTimer(buffer, out timer))
+            {
+                timer.Stop();
+            }
+            else
+            {
+                timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle)
+                {
+                    Interval = TimeSpan.FromMilliseconds(500)
+                };
+
+                timer.Tick += (s, e) =>
+                {
+                    ClearBufferTimer(buffer);
+
+                    HashSet<EventHandler> handlers;
+                    if (TryGetBufferListeners(buffer, out handlers))
+                    {
+                        foreach (var handler in handlers)
+                        {
+                            handler(buffer, new EventArgs());
+                        }
+                    }
+                };
+
+                buffer.Properties[bufferTimerKey] = timer;
+            }
+
+            timer.Start();
+        }
+
+        static void BufferChanged(object sender, TextContentChangedEventArgs e)
+        {
+            ITextBuffer buffer = sender as ITextBuffer;
+            if (buffer == null)
+                return;
+
+            RestartTimerForBuffer(buffer);
+        }
+
+        #endregion
+    }
+
+}
--- a/vs/ext/ClassificationTagger.cs
+++ b/vs/ext/ClassificationTagger.cs
@ -0,0 +1,122 @@
+using System;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using System.Windows.Media;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Classification;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+
+
+namespace IvyLanguage
+{
+
+  #region Provider
+
+  [Export(typeof(ITaggerProvider))]
+  [ContentType("ivy")]
+  [TagType(typeof(ClassificationTag))]
+  internal sealed class IvyClassifierProvider : ITaggerProvider
+  {
+    [Import]
+    internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
+
+    [Import]
+    internal IClassificationTypeRegistryService ClassificationTypeRegistry = null;
+
+    [Import]
+    internal Microsoft.VisualStudio.Language.StandardClassification.IStandardClassificationService Standards = null;
+
+    public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+      ITagAggregator<IvyTokenTag> tagAggregator = AggregatorFactory.CreateTagAggregator<IvyTokenTag>(buffer);
+      return new IvyClassifier(buffer, tagAggregator, ClassificationTypeRegistry, Standards) as ITagger<T>;
+    }
+  }
+
+  #endregion
+
+  #region Tagger
+
+  internal sealed class IvyClassifier : ITagger<ClassificationTag>
+  {
+    ITextBuffer _buffer;
+    ITagAggregator<IvyTokenTag> _aggregator;
+    IDictionary<IvyTokenKind, IClassificationType> _typeMap;
+
+    
+
+    internal IvyClassifier(ITextBuffer buffer,
+                             ITagAggregator<IvyTokenTag> tagAggregator,
+                             IClassificationTypeRegistryService typeService, Microsoft.VisualStudio.Language.StandardClassification.IStandardClassificationService standards) {
+      _buffer = buffer;
+      _aggregator = tagAggregator;
+      _aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
+
+      // use built-in classification types:
+      _typeMap = new Dictionary<IvyTokenKind, IClassificationType>();
+      _typeMap[IvyTokenKind.Keyword] = standards.Keyword;
+      _typeMap[IvyTokenKind.BuiltInType] = standards.Keyword;
+      _typeMap[IvyTokenKind.Number] = standards.NumberLiteral;
+      _typeMap[IvyTokenKind.String] = standards.StringLiteral;
+      _typeMap[IvyTokenKind.Comment] = standards.Comment;
+      _typeMap[IvyTokenKind.VariableIdentifier] = standards.Identifier;
+
+    }
+
+    public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+    public IEnumerable<ITagSpan<ClassificationTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+      if (spans.Count == 0) yield break;
+      var snapshot = spans[0].Snapshot;
+      foreach (var tagSpan in this._aggregator.GetTags(spans)) {
+        IClassificationType t = _typeMap[tagSpan.Tag.Kind];
+        foreach (SnapshotSpan s in tagSpan.Span.GetSpans(snapshot)) {
+          yield return new TagSpan<ClassificationTag>(s, new ClassificationTag(t));
+        }
+      }
+    }
+
+    void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {
+      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));
+        }
+      }
+    }
+  }
+
+  /// <summary>
+  /// Defines an editor format for user-defined type.
+  /// </summary>
+  [Export(typeof(EditorFormatDefinition))]
+  [ClassificationType(ClassificationTypeNames = "Ivy identifier")]
+  [Name("Ivy identifier")]
+  [UserVisible(true)]
+  //set the priority to be after the default classifiers
+  [Order(Before = Priority.Default)]
+  internal sealed class IvyTypeFormat : ClassificationFormatDefinition
+  {
+    public IvyTypeFormat() {
+      this.DisplayName = "Ivy identifier"; //human readable version of the name
+      this.ForegroundColor = Colors.CornflowerBlue;
+    }
+  }
+
+  internal static class ClassificationDefinition
+  {
+    /// <summary>
+    /// Defines the "ordinary" classification type.
+    /// </summary>
+    [Export(typeof(ClassificationTypeDefinition))]
+    [Name("Ivy identifier")]
+    internal static ClassificationTypeDefinition UserType = null;
+  }
+
+
+
+  #endregion
+
+}
--- a/vs/ext/ContentType.cs
+++ b/vs/ext/ContentType.cs
@ -0,0 +1,35 @@
+using System.ComponentModel.Composition;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Utilities;
+
+
+namespace IvyLanguage
+{
+  class IvyContentType
+  {
+    [Export]
+    [Name("ivy")]
+    [BaseDefinition("code")]
+    internal static ContentTypeDefinition ContentType = null;
+
+    [Export(typeof(IWpfTextViewCreationListener))]
+    [ContentType("text")]
+    [TextViewRole(PredefinedTextViewRoles.Document)]
+    internal sealed class IvyTextViewCreationListener : IWpfTextViewCreationListener
+    {
+      [Export(typeof(AdornmentLayerDefinition))]
+      [Name("ModelAdornment")]
+      [Order(After = PredefinedAdornmentLayers.Selection, Before = PredefinedAdornmentLayers.Text)]
+      [TextViewRole(PredefinedTextViewRoles.Document)]
+      public AdornmentLayerDefinition editorAdornmentLayer = null;
+      public void TextViewCreated(IWpfTextView textView)
+      {
+      }
+    }
+
+    [Export]
+    [FileExtension(".ivy")]
+    [ContentType("ivy")]
+    internal static FileExtensionToContentTypeDefinition FileType = null;
+  }
+}
--- a/vs/ext/DafnyDriver.cs
+++ b/vs/ext/DafnyDriver.cs
@ -0,0 +1,380 @@
+using System;
+using System.Collections.Concurrent;
+using System.Collections.Generic;
+using System.Collections.ObjectModel;
+using System.Diagnostics.Contracts;
+using System.IO;
+using System.Linq;
+using Microsoft.Boogie;
+using Microsoft.Ivy;
+using Microsoft.VisualStudio.Text;
+using Bpl = Microsoft.Boogie;
+using Ivy = Microsoft.Ivy;
+
+
+namespace IvyLanguage
+{
+
+  public class IvyDriver
+  {
+    readonly string _filename;
+    readonly ITextSnapshot _snapshot;
+    readonly ITextBuffer _buffer;
+    Ivy.Program _program;
+    static object bufferIvyKey = new object();
+
+    List<IvyError> _errors = new List<IvyError>();
+    public List<IvyError> Errors { get { return _errors; } }
+
+    public IvyDriver(ITextBuffer buffer, string filename) {
+      _buffer = buffer;
+      _snapshot = buffer.CurrentSnapshot;
+      _filename = filename;
+    }
+
+    static IvyDriver() {
+      // TODO(wuestholz): Do we really need to initialze this here?
+      Initialize();
+    }
+
+    static void Initialize() {
+      if (Ivy.IvyOptions.O == null) {
+        var options = new Ivy.IvyOptions();
+        options.ProverKillTime = 10;
+        options.AutoTriggers = true;
+        options.ErrorTrace = 0;
+        options.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1);
+        options.ModelViewFile = "-";
+        options.UnicodeOutput = true;
+        Ivy.IvyOptions.Install(options);
+
+        // Read additional options from IvyOptions.txt
+        string codebase = Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location);
+        string optionsFilePath = Path.Combine(codebase, "IvyOptions.txt");
+        if (File.Exists(optionsFilePath)) {
+          var optionsReader = new StreamReader(new FileStream(optionsFilePath, FileMode.Open, FileAccess.Read));
+          List<string> args = new List<string>();
+          while (true) {
+            string line = optionsReader.ReadLine();
+            if (line == null) break;
+            line = line.Trim();
+            if (line.Length == 0 || line.StartsWith("//")) continue;
+            args.Add(line);
+          }
+          optionsReader.Close();
+          CommandLineOptions.Clo.Parse(args.ToArray());
+        } else {
+          options.ApplyDefaultOptions();
+        }
+
+        ExecutionEngine.printer = new DummyPrinter();
+        ExecutionEngine.errorInformationFactory = new IvyErrorInformationFactory();
+        ChangeIncrementalVerification(2);
+      }
+    }
+
+
+    #region Output
+
+    class DummyPrinter : OutputPrinter
+    {
+      public void AdvisoryWriteLine(string format, params object[] args)
+      {
+      }
+
+      public void ErrorWriteLine(TextWriter tw, string format, params object[] args)
+      {
+      }
+
+      public void ErrorWriteLine(TextWriter tw, string s)
+      {
+      }
+
+      public void Inform(string s, TextWriter tw)
+      {
+      }
+
+      public void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null)
+      {
+      }
+
+      public void WriteTrailer(PipelineStatistics stats)
+      {
+      }
+
+      public void WriteErrorInformation(ErrorInformation errorInfo, TextWriter tw, bool skipExecutionTrace = true)
+      {
+      }
+    }
+
+    #endregion
+
+    #region Parsing and type checking
+
+    internal Ivy.Program ProcessResolution(bool runResolver) {
+      if (!ParseAndTypeCheck(runResolver)) {
+        return null;
+      }
+      return _program;
+    }
+
+    bool ParseAndTypeCheck(bool runResolver) {
+      Tuple<ITextSnapshot, Ivy.Program, List<IvyError>> parseResult;
+      Ivy.Program program;
+      var errorReporter = new VSErrorReporter(this);
+      if (_buffer.Properties.TryGetProperty(bufferIvyKey, out parseResult) &&
+         (parseResult.Item1 == _snapshot)) {
+        // already parsed;
+        program = parseResult.Item2;
+        _errors = parseResult.Item3;
+        if (program == null)
+          runResolver = false;
+      } else {
+        Ivy.ModuleDecl module = new Ivy.LiteralModuleDecl(new Ivy.DefaultModuleDecl(), null);
+        Ivy.BuiltIns builtIns = new Ivy.BuiltIns();
+        var parseErrors = new Ivy.Errors(errorReporter);
+        int errorCount = Ivy.Parser.Parse(_snapshot.GetText(), _filename, _filename, null, module, builtIns, parseErrors);
+        string errString = Ivy.Main.ParseIncludes(module, builtIns, new List<string>(), parseErrors);
+
+        if (errorCount != 0 || errString != null) {
+          runResolver = false;
+          program = null;
+        } else {
+          program = new Ivy.Program(_filename, module, builtIns, errorReporter);
+        }
+        _buffer.Properties[bufferIvyKey] = new Tuple<ITextSnapshot, Ivy.Program, List<IvyError>>(_snapshot, program, _errors);
+      }
+      if (!runResolver) {
+        return false;
+      }
+
+      var r = new Resolver(program);
+      r.ResolveProgram(program);
+      if (errorReporter.Count(ErrorLevel.Error) != 0)
+        return false;
+
+      _program = program;
+      return true;  // success
+    }
+
+
+    void RecordError(string filename, int line, int col, ErrorCategory cat, string msg, bool isRecycled = false)
+    {
+      _errors.Add(new IvyError(filename, line - 1, col - 1, cat, msg, _snapshot, isRecycled, null, System.IO.Path.GetFullPath(this._filename) == filename));
+    }
+
+    class VSErrorReporter : Ivy.ErrorReporter
+    {
+      IvyDriver dd;
+
+      public VSErrorReporter(IvyDriver dd) {
+        this.dd = dd;
+      }
+
+      // TODO: The error tracking could be made better to track the full information returned by Ivy
+      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;
+        }
+      }
+    }
+
+    public class ErrorSink : Bpl.IErrorSink
+    {
+      IvyDriver dd;
+
+      public ErrorSink(IvyDriver dd) {
+        this.dd = dd;
+      }
+      public void Error(Bpl.IToken tok, string msg) {
+        dd.RecordError(tok.filename, tok.line, tok.col, ErrorCategory.VerificationError, msg);
+      }
+    }
+
+    #endregion
+
+    #region Compilation
+
+    public static void Compile(Ivy.Program ivyProgram, TextWriter outputWriter)
+    {
+      Microsoft.Ivy.IvyOptions.O.SpillTargetCode = true;
+      // 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.Ivy.IvyDriver.CompileIvyProgram(ivyProgram, ivyProgram.FullName, otherFileNames, outputWriter);
+    }
+
+    #endregion
+
+    #region Boogie interaction
+
+    class IvyErrorInformationFactory : ErrorInformationFactory
+    {
+      public override ErrorInformation CreateErrorInformation(IToken tok, string msg, string requestId, string originalRequestId, string category = null)
+      {
+        return new IvyErrorInformation(tok, msg, requestId, originalRequestId, category);
+      }
+    }
+
+    class IvyErrorInformation : ErrorInformation
+    {
+      public IvyErrorInformation(IToken tok, string msg, string requestId, string originalRequestId, string category = null)
+        : base(tok, msg)
+      {
+        RequestId = requestId;
+        OriginalRequestId = originalRequestId;
+        Category = category;
+        AddNestingsAsAux(tok);
+      }
+
+      public override void AddAuxInfo(IToken tok, string msg, string category = null)
+      {
+        base.AddAuxInfo(tok, msg, category);
+        AddNestingsAsAux(tok);
+      }
+
+      void AddNestingsAsAux(IToken tok)
+      {
+        while (tok != null && tok is Ivy.NestedToken)
+        {
+          var nt = (Ivy.NestedToken)tok;
+          tok = nt.Inner;
+          Aux.Add(new AuxErrorInfo(tok, "Related location"));
+        }
+      }
+    }
+
+    public static int IncrementalVerificationMode()
+    {
+      return Ivy.IvyOptions.Clo.VerifySnapshots;
+    }
+
+    public static void SetDiagnoseTimeouts(bool v)
+    {
+      Ivy.IvyOptions.Clo.RunDiagnosticsOnTimeout = v;
+    }
+
+    public static int ChangeIncrementalVerification(int mode)
+    {
+      var old = Ivy.IvyOptions.Clo.VerifySnapshots;
+      if (mode == 1 && 1 <= old)
+      {
+        // Disable mode 1.
+        Ivy.IvyOptions.Clo.VerifySnapshots = 0;
+      }
+      else if (mode == 2 && old == 2)
+      {
+        // Disable mode 2.
+        Ivy.IvyOptions.Clo.VerifySnapshots = 1;
+      }
+      else
+      {
+        // Enable mode.
+        Ivy.IvyOptions.Clo.VerifySnapshots = mode;
+      }
+      return Ivy.IvyOptions.Clo.VerifySnapshots;
+    }
+
+    public static bool ChangeAutomaticInduction() {
+      var old = Ivy.IvyOptions.O.Induction;
+      // toggle between modes 1 and 3
+      Ivy.IvyOptions.O.Induction = old == 1 ? 3 : 1;
+      return Ivy.IvyOptions.O.Induction == 3;
+    }
+
+    public bool Verify(Ivy.Program ivyProgram, ResolverTagger resolver, string uniqueIdPrefix, string requestId, ErrorReporterDelegate er) {
+
+      Ivy.Translator translator = new Ivy.Translator(ivyProgram.reporter);
+      var translatorFlags = new Ivy.Translator.TranslatorFlags() { InsertChecksums = true, UniqueIdPrefix = uniqueIdPrefix };
+
+
+      var boogiePrograms = Ivy.Translator.Translate(ivyProgram, ivyProgram.reporter, translatorFlags);
+
+      var impls = boogiePrograms.SelectMany(p => p.Item2.Implementations);
+      resolver.ReInitializeVerificationErrors(requestId, impls);
+
+      bool success = false;
+      var errorSink = new ErrorSink(this);
+      
+      foreach (var kv in boogiePrograms) {
+        var boogieProgram = kv.Item2;
+
+        // TODO(wuestholz): Maybe we should use a fixed program ID to limit the memory overhead due to the program cache in Boogie.
+        PipelineOutcome oc = BoogiePipeline(boogieProgram, 1 < Ivy.DafnyOptions.Clo.VerifySnapshots ? uniqueIdPrefix : null, requestId, errorSink, er);
+        switch (oc) {
+          case PipelineOutcome.Done:
+          case PipelineOutcome.VerificationCompleted:
+            // TODO:  This would be the place to proceed to compile the program, if desired
+            success = true;
+            break;
+          case PipelineOutcome.FatalError:
+          default:
+            return false;
+        }
+      }
+      return success;
+    }
+
+    /// <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(Bpl.Program/*!*/ program, string programId, string requestId, ErrorSink errorSink, ErrorReporterDelegate er)
+    {
+      Contract.Requires(program != null);
+
+      PipelineOutcome oc = BoogieResolveAndTypecheck(program, errorSink);
+      if (oc == PipelineOutcome.ResolvedAndTypeChecked) {
+        ExecutionEngine.EliminateDeadVariables(program);
+        ExecutionEngine.CollectModSets(program);
+        ExecutionEngine.CoalesceBlocks(program);
+        ExecutionEngine.Inline(program);
+        return ExecutionEngine.InferAndVerify(program, new PipelineStatistics(), programId, er, requestId);
+      }
+      return oc;
+    }
+
+    /// <summary>
+    /// Resolves and type checks the given Boogie program.
+    /// 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 BoogieResolveAndTypecheck(Bpl.Program program, ErrorSink errorSink) {
+      Contract.Requires(program != null);
+      // ---------- Resolve ------------------------------------------------------------
+      int errorCount = program.Resolve(errorSink);
+      if (errorCount != 0) {
+        return PipelineOutcome.ResolutionError;
+      }
+
+      // ---------- Type check ------------------------------------------------------------
+      errorCount = program.Typecheck(errorSink);
+      if (errorCount != 0) {
+        return PipelineOutcome.TypeCheckingError;
+      }
+
+      return PipelineOutcome.ResolvedAndTypeChecked;
+    }
+
+    #endregion
+  }
+
+}
--- a/vs/ext/ErrorModelTagger.cs
+++ b/vs/ext/ErrorModelTagger.cs
@ -0,0 +1,307 @@
+using System;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using System.Linq;
+using System.Windows;
+using System.Windows.Controls;
+using System.Windows.Input;
+using System.Windows.Media;
+using System.Windows.Shapes;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+
+
+namespace DafnyLanguage
+{
+
+  #region Provider
+
+  [Export(typeof(IViewTaggerProvider))]
+  [ContentType("dafny")]
+  [Name("ErrorModelTagger")]
+  [Order(After = "ProgressTagger")]
+  [TextViewRole(PredefinedTextViewRoles.Document)]
+  [TagType(typeof(IntraTextAdornmentTag))]
+  internal sealed class ErrorModelTaggerProvider : IViewTaggerProvider
+  {
+    [Import]
+    internal IBufferTagAggregatorFactoryService BufferTagAggregatorFactoryService = null;
+
+    public ITagger<T> CreateTagger<T>(ITextView textView, ITextBuffer buffer) where T : ITag
+    {
+      if (textView == null)
+        throw new ArgumentNullException("textView");
+
+      if (buffer == null)
+        throw new ArgumentNullException("buffer");
+
+      if (buffer != textView.TextBuffer)
+        return null;
+
+      return ErrorModelTagger.GetTagger(
+                (IWpfTextView)textView,
+                new Lazy<ITagAggregator<IDafnyResolverTag>>(
+                    () => BufferTagAggregatorFactoryService.CreateTagAggregator<IDafnyResolverTag>(textView.TextBuffer)))
+                as ITagger<T>;
+    }
+  }
+
+  #endregion
+
+
+  #region Tagger
+
+  internal sealed class ErrorModelTagger : ITagger<IntraTextAdornmentTag>, IDisposable
+  {
+    IWpfTextView _view;
+    ITagAggregator<IDafnyResolverTag> _aggregator;
+
+    internal static ITagger<IntraTextAdornmentTag> GetTagger(IWpfTextView view, Lazy<ITagAggregator<IDafnyResolverTag>> aggregator)
+    {
+      return view.Properties.GetOrCreateSingletonProperty<ErrorModelTagger>(
+            () => new ErrorModelTagger(view, aggregator.Value));
+    }
+
+    private ErrorModelTagger(IWpfTextView view, ITagAggregator<IDafnyResolverTag> aggregator)
+    {
+      _view = view;
+      _aggregator = aggregator;
+      _aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
+    }
+
+    public void Dispose()
+    {
+      _aggregator.Dispose();
+      _view.Properties.RemoveProperty(typeof(ErrorModelTagger));
+    }
+
+    public IEnumerable<ITagSpan<IntraTextAdornmentTag>> GetTags(NormalizedSnapshotSpanCollection spans)
+    {
+      if (spans.Count == 0) yield break;
+      var snapshot = spans[0].Snapshot;
+
+      var adornmentsPerSnapshot = new Dictionary<SnapshotSpan, List<Ellipse>>();
+      foreach (var tag in _aggregator.GetTags(spans))
+      {
+        var ertag = tag.Tag as DafnyErrorResolverTag;
+        if (ertag != null && ertag.Error.ModelText != null)
+        {
+          NormalizedSnapshotSpanCollection normSpans = tag.Span.GetSpans(snapshot);
+
+          if (normSpans.Count != 1)
+            continue;
+
+          var adornment = _view.VisualElement.Dispatcher.Invoke(() => CreateErrorAdornment(ertag));
+          var span = new SnapshotSpan(normSpans[0].Start, 0);
+          List<Ellipse> adornments;
+          if (adornmentsPerSnapshot.TryGetValue(span, out adornments))
+          {
+            adornments.Add(adornment);
+          }
+          else
+          {
+            adornmentsPerSnapshot.Add(span, new List<Ellipse> { adornment });
+          }
+        }
+
+        var esrtag = tag.Tag as DafnyErrorStateResolverTag;
+        if (esrtag != null)
+        {
+          var adornment = _view.VisualElement.Dispatcher.Invoke(() => CreateErrorStateAdornment(esrtag));
+          var span = esrtag.Span.GetSpan(snapshot);
+          List<Ellipse> adornments;
+          if (adornmentsPerSnapshot.TryGetValue(span, out adornments))
+          {
+            adornments.Add(adornment);
+          }
+          else
+          {
+            adornmentsPerSnapshot.Add(span, new List<Ellipse> { adornment });
+          }
+        }
+      }
+
+      foreach (var adornments in adornmentsPerSnapshot)
+      {
+        var panel = _view.VisualElement.Dispatcher.Invoke(() =>
+        {
+          var maxConcurrentAdornments = adornments.Value.Where(a => a.Fill == Brushes.Crimson).Count()    // number of error adornments
+                                        + (adornments.Value.Any(a => a.Fill != Brushes.Crimson) ? 1 : 0); // number of error state adornments
+          var p = new StackPanel
+          {
+            Orientation = Orientation.Horizontal,
+            Width = 12.0 * maxConcurrentAdornments,
+            Height = 12.0,
+          };
+          foreach (var adornment in adornments.Value)
+          {
+            p.Children.Add(adornment);
+          }
+          p.Measure(new Size(double.PositiveInfinity, double.PositiveInfinity));
+          return p;
+        });
+
+        yield return new TagSpan<IntraTextAdornmentTag>(adornments.Key, new IntraTextAdornmentTag(panel, null, PositionAffinity.Successor));
+      }
+    }
+
+    private static string ErrorStateToolTip(bool isSelected, string description)
+    {
+      return string.Format("{0}{1}", isSelected ? "unselect state" : "select state", !string.IsNullOrEmpty(description) ? " [" + description + "]" : "");
+    }
+
+    private Ellipse CreateErrorStateAdornment(DafnyErrorStateResolverTag esrtag)
+    {
+      var result = new Ellipse
+      {
+        Fill = Brushes.DodgerBlue,
+        Height = 12.0,
+        Width = 12.0,
+        ToolTip = ErrorStateToolTip(false, esrtag.Description),
+        StrokeThickness = 3.0,
+        Stroke = Brushes.DodgerBlue,
+        Cursor = Cursors.Arrow,
+        Visibility = System.Windows.Visibility.Collapsed
+      };
+
+      esrtag.Error.StateChangeEvent += new DafnyError.StateChangeEventHandler((o) =>
+      {
+        _view.VisualElement.Dispatcher.Invoke(() =>
+          {
+            result.Visibility = esrtag.Error.IsSelected ? System.Windows.Visibility.Visible : System.Windows.Visibility.Collapsed;
+            var isSelected = esrtag.Error.IsSelected && esrtag.Error.SelectedStateId == esrtag.Id;
+            result.Stroke = isSelected ? Brushes.Black : Brushes.DodgerBlue;
+            if (isSelected)
+            {
+              result.ToolTip = ErrorStateToolTip(isSelected, esrtag.Description);
+              esrtag.Error.SelectedStateAdornment = result;
+            }
+          });
+      });
+
+      result.MouseDown += new MouseButtonEventHandler((s, e) =>
+      {
+        _view.VisualElement.Dispatcher.Invoke(() =>
+          {
+            if (!esrtag.Error.IsSelected) { return; }
+            if (esrtag.Error.SelectedStateAdornment == result)
+            {
+              // unselect it
+              esrtag.Error.SelectedStateAdornment = null;
+              esrtag.Error.SelectedStateId = -1;
+              result.Stroke = Brushes.DodgerBlue;
+              result.ToolTip = result.ToolTip.ToString().Replace("unselect", "select");
+            }
+            else
+            {
+              // unselect the old one
+              if (esrtag.Error.SelectedStateAdornment != null)
+              {
+                esrtag.Error.SelectedStateAdornment.Stroke = Brushes.DodgerBlue;
+                esrtag.Error.SelectedStateAdornment.ToolTip = esrtag.Error.SelectedStateAdornment.ToolTip.ToString().Replace("unselect", "select");
+                esrtag.Error.SelectedStateAdornment = null;
+                esrtag.Error.SelectedStateId = -1;
+              }
+
+              // select the new one
+              esrtag.Error.SelectedStateAdornment = result;
+              esrtag.Error.SelectedStateAdornment.Stroke = Brushes.Black;
+              esrtag.Error.SelectedStateAdornment.ToolTip = ErrorStateToolTip(true, esrtag.Description);
+              esrtag.Error.SelectedStateId = esrtag.Id;
+              if (!string.IsNullOrEmpty(esrtag.Error.ModelText))
+              {
+                DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(esrtag.Error.ModelText, esrtag.Id);
+              }
+            }
+          });
+      });
+      return result;
+    }
+
+    private Ellipse CreateErrorAdornment(DafnyErrorResolverTag ertag)
+    {
+      var result = new Ellipse
+      {
+        Fill = Brushes.Crimson,
+        Height = 12.0,
+        Width = 12.0,
+        ToolTip = "select error",
+        StrokeThickness = 3.0,
+        Stroke = Brushes.Crimson,
+        Cursor = Cursors.Arrow,
+      };
+
+      result.Measure(new Size(double.PositiveInfinity, double.PositiveInfinity));
+      result.MouseDown += new MouseButtonEventHandler((s, e) =>
+      {
+        _view.VisualElement.Dispatcher.Invoke(() =>
+          {
+            if (ertag.Error.IsSelected)
+            {
+              // unselect it
+              var selErr = ertag.Error.SelectedError;
+              selErr.SelectedStateId = -1;
+              selErr.SelectedStateAdornment = null;
+              ertag.Error.SelectedError = null;
+              result.Stroke = Brushes.Crimson;
+              result.ToolTip = "select error";
+              selErr.Notify();
+            }
+            else
+            {
+              // unselect the old one
+              if (ertag.Error.SelectedError != null)
+              {
+                var selErr = ertag.Error.SelectedError;
+                selErr.SelectedStateId = -1;
+                selErr.SelectedStateAdornment = null;
+                selErr.Adornment.Stroke = Brushes.Crimson;
+                selErr.Adornment.ToolTip = "select error";
+                ertag.Error.SelectedError = null;
+                selErr.Notify();
+              }
+
+              // select the new one
+              ertag.Error.SelectedError = ertag.Error;
+              ertag.Error.Adornment = result;
+              ertag.Error.Adornment.Stroke = Brushes.Black;
+              ertag.Error.Adornment.ToolTip = "unselect error";
+              if (!string.IsNullOrEmpty(ertag.Error.ModelText))
+              {
+                // select the last error state
+                ertag.Error.SelectedStateId = ertag.Error.Model.States.Count() - 1;
+                ertag.Error.SelectedStateAdornment = null;
+                DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(ertag.Error.ModelText, ertag.Error.SelectedStateId);
+              }
+              ertag.Error.SelectedError.Notify();
+            }
+          });
+      });
+      return result;
+    }
+
+    public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+    void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e)
+    {
+      var chng = TagsChanged;
+      if (chng != null)
+      {
+        NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_view.TextBuffer.CurrentSnapshot);
+        if (spans.Count > 0)
+        {
+          SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);
+          _view.VisualElement.Dispatcher.Invoke(() =>
+            {
+              chng(this, new SnapshotSpanEventArgs(span));
+            });
+        }
+      }
+    }
+  }
+
+  #endregion
+
+}
--- a/vs/ext/ErrorTagger.cs
+++ b/vs/ext/ErrorTagger.cs
@ -0,0 +1,83 @@
+using System;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+
+
+namespace DafnyLanguage
+{
+
+  #region Provider
+
+  [Export(typeof(ITaggerProvider))]
+  [Name("ErrorTagger")]
+  [ContentType("dafny")]
+  [TagType(typeof(IErrorTag))]
+  internal sealed class ErrorTaggerProvider : ITaggerProvider
+  {
+    [Import]
+    internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
+
+    public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+      ITagAggregator<IDafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<IDafnyResolverTag>(buffer);
+      // create a single tagger for each buffer.
+      Func<ITagger<T>> sc = delegate() { return new ErrorTagger(buffer, tagAggregator) as ITagger<T>; };
+      return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
+    }
+  }
+
+  #endregion
+
+
+  #region Tagger
+
+  /// <summary>
+  /// Translate PkgDefTokenTags into ErrorTags and Error List items
+  /// </summary>
+  internal sealed class ErrorTagger : ITagger<IErrorTag>
+  {
+    ITextBuffer _buffer;
+    ITagAggregator<IDafnyResolverTag> _aggregator;
+
+    internal ErrorTagger(ITextBuffer buffer, ITagAggregator<IDafnyResolverTag> 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<IErrorTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+      if (spans.Count == 0) yield break;
+      var snapshot = spans[0].Snapshot;
+      foreach (var tagSpan in _aggregator.GetTags(spans)) {
+        var et = tagSpan.Tag as IErrorTag;
+        if (et != null) {
+          foreach (SnapshotSpan s in tagSpan.Span.GetSpans(snapshot)) {
+            yield return new TagSpan<IErrorTag>(s, et);
+          }
+        }
+      }
+    }
+
+    // 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 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));
+        }
+      }
+    }
+  }
+
+  #endregion
+
+}
--- a/vs/ext/GlobalSuppressions.cs
+++ b/vs/ext/GlobalSuppressions.cs
@ -0,0 +1,4 @@
+[assembly: System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Design", "CA1017:MarkAssembliesWithComVisible")]
+[assembly: System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Naming", "CA1703:ResourceStringsShouldBeSpelledCorrectly", MessageId = "Ivy", Scope = "resource", Target = "VSPackage.resources")]
+[assembly: System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Naming", "CA1704:IdentifiersShouldBeSpelledCorrectly", MessageId = "Ivy")]
+[assembly: System.Diagnostics.CodeAnalysis.SuppressMessage("Microsoft.Naming", "CA1704:IdentifiersShouldBeSpelledCorrectly", MessageId = "Ivy", Scope = "type", Target = "IvyLanguage.IvyMenu.IvyMenuPackage")]
--- a/vs/ext/HoverText.cs
+++ b/vs/ext/HoverText.cs
@ -0,0 +1,141 @@
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using System.Linq;
+using Microsoft.VisualStudio.Language.Intellisense;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+
+
+namespace IvyLanguage
+{
+
+  #region Source Provider
+
+  [Export(typeof(IQuickInfoSourceProvider))]
+  [ContentType("ivy")]
+  [Name("Ivy QuickInfo")]
+  class IvyQuickInfoSourceProvider : IQuickInfoSourceProvider
+  {
+    [Import]
+    IBufferTagAggregatorFactoryService aggService = null;
+
+    public IQuickInfoSource TryCreateQuickInfoSource(ITextBuffer textBuffer) {
+      return new IvyQuickInfoSource(textBuffer, aggService.CreateTagAggregator<IvyTokenTag>(textBuffer));
+    }
+  }
+
+  class IvyQuickInfoSource : IQuickInfoSource
+  {
+    private ITagAggregator<IvyTokenTag> _aggregator;
+    private ITextBuffer _buffer;
+
+    public IvyQuickInfoSource(ITextBuffer buffer, ITagAggregator<IvyTokenTag> aggregator)
+    {
+      _aggregator = aggregator;
+      _buffer = buffer;
+    }
+
+    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<IvyTokenTag> curTag in _aggregator.GetTags(new SnapshotSpan(triggerPoint, triggerPoint)))
+      {
+        var s = curTag.Tag.HoverText;
+        if (s != null)
+        {
+          var tagSpan = curTag.Span.GetSpans(_buffer).First();
+          applicableToSpan = _buffer.CurrentSnapshot.CreateTrackingSpan(tagSpan, SpanTrackingMode.EdgeExclusive);
+          quickInfoContent.Add(s);
+        }
+      }
+    }
+    public void Dispose()
+    {
+    }
+  }
+
+  #endregion
+
+
+  #region Controller Provider
+
+  [Export(typeof(IIntellisenseControllerProvider))]
+  [Name("Ivy QuickInfo controller")]
+  [ContentType("ivy")]
+  class IvyQuickInfoControllerProvider : IIntellisenseControllerProvider
+  {
+    [Import]
+    internal IQuickInfoBroker QuickInfoBroker { get; set; }
+
+    public IIntellisenseController TryCreateIntellisenseController(ITextView textView, IList<ITextBuffer> subjectBuffers) {
+      return new IvyQuickInfoController(textView, subjectBuffers, this);
+    }
+  }
+
+  #endregion
+
+
+  #region Controller
+
+  class IvyQuickInfoController : IIntellisenseController
+  {
+    private ITextView _textView;
+    private IList<ITextBuffer> _subjectBuffers;
+    private IvyQuickInfoControllerProvider _componentContext;
+
+    private IQuickInfoSession _session;
+
+    internal IvyQuickInfoController(ITextView textView, IList<ITextBuffer> subjectBuffers, IvyQuickInfoControllerProvider componentContext) {
+      _textView = textView;
+      _subjectBuffers = subjectBuffers;
+      _componentContext = componentContext;
+
+      _textView.MouseHover += this.OnTextViewMouseHover;
+    }
+
+    public void ConnectSubjectBuffer(ITextBuffer subjectBuffer) {
+    }
+
+    public void DisconnectSubjectBuffer(ITextBuffer subjectBuffer) {
+    }
+
+    public void Detach(ITextView textView) {
+      if (_textView == textView) {
+        _textView.MouseHover -= OnTextViewMouseHover;
+        _textView = null;
+      }
+    }
+
+    void OnTextViewMouseHover(object sender, MouseHoverEventArgs e) {
+      SnapshotPoint? point = GetMousePosition(new SnapshotPoint(_textView.TextSnapshot, e.Position));
+
+      if (point != null) {
+        ITrackingPoint triggerPoint = point.Value.Snapshot.CreateTrackingPoint(point.Value.Position, PointTrackingMode.Positive);
+
+        // Find the broker for this buffer
+        if (!_componentContext.QuickInfoBroker.IsQuickInfoActive(_textView)) {
+          _session = _componentContext.QuickInfoBroker.CreateQuickInfoSession(_textView, triggerPoint, true);
+          _session.Start();
+        }
+      }
+    }
+
+    SnapshotPoint? GetMousePosition(SnapshotPoint topPosition) {
+      return _textView.BufferGraph.MapDownToFirstMatch(
+        topPosition,
+        PointTrackingMode.Positive,
+        snapshot => _subjectBuffers.Contains(snapshot.TextBuffer),
+        PositionAffinity.Predecessor);
+    }
+  }
+
+  #endregion
+
+}
--- a/vs/ext/IdentifierTagger.cs
+++ b/vs/ext/IdentifierTagger.cs
@ -0,0 +1,569 @@
+using System;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using System.Diagnostics.Contracts;
+using Microsoft.Ivy;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+using Bpl = Microsoft.Boogie;
+
+namespace IvyLanguage
+{
+
+  #region Provider
+
+  [Export(typeof(ITaggerProvider))]
+  [ContentType("ivy")]
+  [TagType(typeof(IvyTokenTag))]
+  internal sealed class IdentifierTaggerProvider : ITaggerProvider
+  {
+    [Import]
+    internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
+
+    public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+      ITagAggregator<IIvyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<IIvyResolverTag>(buffer);
+      // create a single tagger for each buffer.
+      Func<ITagger<T>> sc = delegate() { return new IdentifierTagger(buffer, tagAggregator) as ITagger<T>; };
+      return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
+    }
+  }
+
+  #endregion
+
+
+  #region Tagger
+
+  /// <summary>
+  /// Translate IvyResolverTag's into IOutliningRegionTag's
+  /// </summary>
+  internal sealed class IdentifierTagger : ITagger<IvyTokenTag>
+  {
+    ITextBuffer _buffer;
+    ITextSnapshot _snapshot;  // the most recent snapshot of _buffer that we have been informed about
+    Microsoft.Ivy.Program _program;  // the program parsed from _snapshot
+    List<IdRegion> _regions = new List<IdRegion>();  // the regions generated from _program
+    public Dictionary<SnapshotSpan, Bpl.IToken> _definitions = new Dictionary<SnapshotSpan, Bpl.IToken>();
+    ITagAggregator<IIvyResolverTag> _aggregator;
+
+    public static readonly IDictionary<ITextBuffer, IdentifierTagger> IdentifierTaggers = new Dictionary<ITextBuffer, IdentifierTagger>();
+
+
+    internal IdentifierTagger(ITextBuffer buffer, ITagAggregator<IIvyResolverTag> tagAggregator) {
+      _buffer = buffer;
+      _snapshot = _buffer.CurrentSnapshot;
+      _aggregator = tagAggregator;
+      _aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
+      IdentifierTaggers[_buffer] = this;
+    }
+
+    /// <summary>
+    /// Find the Error tokens in the set of all tokens and create an ErrorTag for each
+    /// </summary>
+    public IEnumerable<ITagSpan<IvyTokenTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+      if (spans.Count == 0) yield break;
+      // (A NormalizedSnapshotSpanCollection contains spans that all come from the same snapshot.)
+      // The spans are ordered by the .Start component, and the collection contains no adjacent or abutting spans.
+      // Hence, to find a span that includes all the ones in "spans", we only need to look at the .Start for the
+      // first spand and the .End of the last span:
+      var startPoint = spans[0].Start;
+      var endPoint = spans[spans.Count - 1].End;
+
+      // Note, (startPoint,endPoint) are points in the spans for which we're being asked to provide tags.  We need to translate
+      // these back into the most recent snapshot that we've computed regions for, namely _snapshot.
+      var entire = new SnapshotSpan(startPoint, endPoint).TranslateTo(_snapshot, SpanTrackingMode.EdgeExclusive);
+      int start = entire.Start;
+      int end = entire.End;
+      foreach (var r in _regions) {
+        if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) {
+          IvyTokenKind kind;
+          switch (r.Kind) {
+            case IdRegion.OccurrenceKind.Use:
+              kind = IvyTokenKind.VariableIdentifier; break;
+            case IdRegion.OccurrenceKind.Definition:
+              kind = IvyTokenKind.VariableIdentifierDefinition; break;
+            case IdRegion.OccurrenceKind.WildDefinition:
+              kind = IvyTokenKind.Keyword; break;
+            case IdRegion.OccurrenceKind.AdditionalInformation:
+              kind = IvyTokenKind.AdditionalInformation; break;
+            case IdRegion.OccurrenceKind.Attribute:
+              kind = IvyTokenKind.Attribute; break;
+            case IdRegion.OccurrenceKind.RecognizedAttributeId:
+              kind = IvyTokenKind.RecognizedAttributeId; break;
+            default:
+              Contract.Assert(false);  // unexpected OccurrenceKind
+              goto case IdRegion.OccurrenceKind.Use;  // to please compiler
+          }
+          yield return new TagSpan<IvyTokenTag>(
+            new SnapshotSpan(_snapshot, r.Start, r.Length),
+            new IvyTokenTag(kind, r.HoverText, r.Variable));
+        }
+      }
+    }
+
+    // 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) {
+        ITextSnapshot snap;
+        Microsoft.Ivy.Program prog;
+        lock (this) {
+          snap = r.Snapshot;
+          prog = r.Program;
+        }
+        if (prog != null) {
+          if (!ComputeIdentifierRegions(prog, snap))
+            return;  // no new regions
+
+          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));
+            }
+          }
+        }
+      }
+    }
+
+    bool ComputeIdentifierRegions(Microsoft.Ivy.Program program, ITextSnapshot snapshot) {
+      Contract.Requires(snapshot != null);
+
+      if (program == _program)
+        return false;  // no new regions
+
+      _snapshot = snapshot;
+      List<IdRegion> newRegions = new List<IdRegion>();
+
+      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()) {
+        if (module.IsFacade) {
+          continue;
+        }
+        foreach (var d in module.TopLevelDecls) {
+          IdRegion.AddRecognizedAttributes(d.Attributes, newRegions, program);
+          if (d is DatatypeDecl) {
+            var dt = (DatatypeDecl)d;
+            foreach (var ctor in dt.Ctors) {
+              foreach (var dtor in ctor.Destructors) {
+                if (dtor.CorrespondingFormal.HasName) {
+                  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, program, p.tok, p, true, iter, module);
+            }
+            foreach (var p in iter.Outs) {
+              IdRegion.Add(newRegions, program, p.tok, p, true, "yield-parameter", iter, 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, program, module));
+            }
+            if (iter.Body != null) {
+              StatementRegions(iter.Body, newRegions, program, module);
+            }
+
+          } else if (d is ClassDecl) {
+            var cl = (ClassDecl)d;
+            foreach (var member in cl.Members) {
+              IdRegion.AddRecognizedAttributes(member.Attributes, newRegions, program);
+              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, program, p.tok, p, true, f, 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, program, module);
+                }
+              } else if (member is Method) {
+                var m = (Method)member;
+                foreach (var p in m.Ins) {
+                  IdRegion.Add(newRegions, program, p.tok, p, true, m, module);
+                }
+                foreach (var p in m.Outs) {
+                  IdRegion.Add(newRegions, program, p.tok, p, true, m, 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, program, module);
+                }
+              } else if (member is SpecialField) {
+                // do nothing
+              } else if (member is Field) {
+                var fld = (Field)member;
+                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, program, dd.Var.tok, dd.Var, true, (ICallable)null, module);
+              ExprRegions(dd.Constraint, newRegions, program, module);
+            }
+          }
+        }
+      }
+      _regions = newRegions;
+      _program = program;
+      return true;
+    }
+
+    void FrameExprRegions(FrameExpression fe, List<IdRegion> regions, bool descendIntoExpressions, Microsoft.Ivy.Program prog, ModuleDefinition module) {
+      Contract.Requires(fe != null);
+      Contract.Requires(regions != null);
+      Contract.Requires(prog != null);
+      if (descendIntoExpressions) {
+        ExprRegions(fe.E, regions, prog, module);
+      }
+      if (fe.Field != null) {
+        Microsoft.Ivy.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, prog, fe.tok, fe.Field, showType, "field", false, module);
+        RecordUseAndDef(prog, fe.tok, fe.Field.Name.Length, fe.Field.tok);
+      }
+    }
+
+    void ExprRegions(Microsoft.Ivy.Expression expr, List<IdRegion> regions, Microsoft.Ivy.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, prog, e.tok, e.Var, false, (ICallable)null, module);
+      } else if (expr is MemberSelectExpr) {
+        var e = (MemberSelectExpr)expr;
+        var field = e.Member as Field;
+        if (field != null) {
+          IdRegion.Add(regions, prog, e.tok, field, e.Type, "field", false, module);
+        }
+        if (e.Member != null) {
+          RecordUseAndDef(prog, e.tok, e.Member.Name.Length, e.Member.tok);
+        }
+      } else if (expr is FunctionCallExpr) {
+        var e = (FunctionCallExpr)expr;
+        var func = e.Function;
+        if (func != null) {
+          RecordUseAndDef(prog, e.tok, func.Name.Length, func.tok);
+        }
+      } else if (expr is ApplySuffix) {
+         // No need to call ExprRegions on the Lhs field because the for loop at the end of this function will do that.
+      } else if (expr is LetExpr) {
+        var e = (LetExpr)expr;
+        IdRegion.AddRecognizedAttributes(e.Attributes, regions, prog);
+        foreach (var bv in e.BoundVars) {
+          IdRegion.Add(regions, prog, bv.tok, bv, true, (ICallable)null, module);
+        }
+      } else if (expr is ComprehensionExpr) {
+        var e = (ComprehensionExpr)expr;
+        IdRegion.AddRecognizedAttributes(e.Attributes, regions, prog);
+        foreach (var bv in e.BoundVars) {
+          IdRegion.Add(regions, prog, bv.tok, bv, true, (ICallable)null, module);
+        }
+      } else if (expr is MatchExpr) {
+        var e = (MatchExpr)expr;
+        foreach (var kase in e.Cases) {
+          kase.Arguments.ForEach(bv => {
+            IdRegion.Add(regions, prog, bv.tok, bv, true, (ICallable)null, 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, (ICallable)null, 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, prog, module));
+        return;  // return here, so as to avoid doing the subexpressions below
+      }
+      foreach (var ee in expr.SubExpressions) {
+        ExprRegions(ee, regions, prog, module);
+      }
+    }
+
+    void RecordUseAndDef(Program prog, Bpl.IToken useTok, int length, Bpl.IToken defTok) {
+      if (prog.FullName.ToLower().CompareTo(useTok.filename.ToLower()) == 0) {  // Otherwise, we're looking at an included file
+        // add to the definition table so we know where the definition for this expr is
+        SnapshotSpan span = new SnapshotSpan(this._snapshot, useTok.pos, length);
+        if (!_definitions.ContainsKey(span)) {
+          _definitions.Add(span, defTok);
+        }
+      }
+    }
+
+    public bool FindDefinition(int caretPos, out string fileName, out int lineNumber, out int offset) {
+      foreach (var use in _definitions.Keys) {
+        if (caretPos >= use.Start && caretPos <= use.End) {
+          // go to the source
+          Bpl.IToken tok;
+          if (_definitions.TryGetValue(use, out tok)) {
+            fileName = tok.filename;
+            lineNumber = tok.line - 1;
+            offset = tok.col - 1;
+            return true;
+          }
+        }
+      }
+      fileName = null;
+      lineNumber = offset = 0;
+      return false;
+    }
+
+    void StatementRegions(Statement stmt, List<IdRegion> regions, Microsoft.Ivy.Program prog, ModuleDefinition module) {
+      Contract.Requires(stmt != null);
+      Contract.Requires(regions != null);
+      Contract.Requires(prog != null);
+      IdRegion.AddRecognizedAttributes(stmt.Attributes, regions, prog);
+      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.AddRecognizedAttributes(local.Attributes, regions, prog);
+          IdRegion.Add(regions, prog, local.Tok, local, true, (ICallable)null, module);
+        }
+        if (s.Update == null) {
+          // the VarDeclStmt has no associated assignment
+        } else if (s.Update is UpdateStmt) {
+          var upd = (UpdateStmt)s.Update;
+          foreach (var rhs in upd.Rhss) {
+            foreach (var ee in rhs.SubExpressions) {
+              ExprRegions(ee, regions, prog, module);
+            }
+            if (rhs is TypeRhs) {
+              CallStmt call = ((TypeRhs)rhs).InitCall;
+              if (call != null) {
+                var method = call.Method;
+                if (method != null) {
+                  if (method is Constructor) {
+                    // call token starts at the beginning of "new C()", so we need to add 4 to the length.
+                    RecordUseAndDef(prog, call.Tok, method.EnclosingClass.Name.Length+4, method.EnclosingClass.tok);
+                  } else {
+                    RecordUseAndDef(prog, call.Tok, method.Name.Length, method.tok);
+                  }
+                }
+              }
+            }
+          }
+        } else {
+          var upd = (AssignSuchThatStmt)s.Update;
+          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, prog, bv.tok, bv, true, (ICallable)null, module));
+      } else if (stmt is MatchStmt) {
+        var s = (MatchStmt)stmt;
+        foreach (var kase in s.Cases) {
+          kase.Arguments.ForEach(bv => {
+            IdRegion.Add(regions, prog, bv.tok, bv, true, (ICallable)null, 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, (ICallable)null, module);
+              }
+            }              
+          });
+        }
+      } else if (stmt is LoopStmt) {
+        var s = (LoopStmt)stmt;
+        if (s.Mod.Expressions != null) {
+          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, prog, module);
+        }
+        foreach (var ss in stmt.SubStatements) {
+          StatementRegions(ss, regions, prog, module);
+        }
+        return;
+      } else if (stmt is CallStmt) {
+        var s = (CallStmt)stmt;
+        var method = s.Method;
+        if (method != null) {
+          RecordUseAndDef(prog, s.MethodSelect.tok, method.Name.Length, method.tok);
+        }
+      }
+      foreach (var ee in stmt.SubExpressions) {
+        ExprRegions(ee, regions, prog, module);
+      }
+      foreach (var ss in stmt.SubStatements) {
+        StatementRegions(ss, regions, prog, module);
+      }
+    }
+
+    class IdRegion : IvyRegion
+    {
+      public readonly int Start;
+      public readonly int Length;
+      public readonly string HoverText;
+      public enum OccurrenceKind { Use, Definition, WildDefinition, AdditionalInformation, Attribute, RecognizedAttributeId }
+      public readonly OccurrenceKind Kind;
+      public readonly IVariable Variable;
+
+      public static void Add(List<IdRegion> regions, Microsoft.Ivy.Program prog, Bpl.IToken tok, IVariable v, bool isDefinition, ICallable callableContext, ModuleDefinition context) {
+        Contract.Requires(regions != null);
+        Contract.Requires(prog != null);
+        Contract.Requires(tok != null);
+        Contract.Requires(v != null);
+        Add(regions, prog, tok, v, isDefinition, null, callableContext, context);
+      }
+      public static void Add(List<IdRegion> regions, Microsoft.Ivy.Program prog, Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ICallable callableContext, ModuleDefinition context) {
+        Contract.Requires(regions != null);
+        Contract.Requires(prog != null);
+        Contract.Requires(tok != null);
+        Contract.Requires(v != null);
+        if (InMainFileAndUserDefined(prog, tok)) {
+          regions.Add(new IdRegion(tok, v, isDefinition, kind, callableContext, context));
+        }
+      }
+      public static void Add(List<IdRegion> regions, Microsoft.Ivy.Program prog, Bpl.IToken tok, Field decl, Microsoft.Ivy.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 (InMainFileAndUserDefined(prog, tok)) {
+          regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context));
+        }
+      }
+
+      public static void Add(List<IdRegion> regions, Microsoft.Ivy.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 (InMainFileAndUserDefined(prog, tok)) {
+          regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length));
+        }
+      }
+
+      public static void AddRecognizedAttributes(Attributes attrs, List<IdRegion> regions, Microsoft.Ivy.Program prog) {
+        Contract.Requires(regions != null);
+        Contract.Requires(prog != null);
+        foreach (var a in attrs.AsEnumerable()) {
+          var usa = a as UserSuppliedAttributes;
+          if (usa != null && InMainFileAndUserDefined(prog, usa.tok)) {
+            regions.Add(new IdRegion(usa.OpenBrace, usa.CloseBrace, OccurrenceKind.Attribute));
+            if (usa.Recognized) {
+              if (usa.Colon.pos + usa.Colon.val.Length == usa.tok.pos) {
+                // just do one highlight
+                regions.Add(new IdRegion(usa.Colon, OccurrenceKind.RecognizedAttributeId, null, usa.Colon.val.Length + usa.tok.val.Length));
+              } else {
+                regions.Add(new IdRegion(usa.Colon, OccurrenceKind.RecognizedAttributeId, null, usa.Colon.val.Length));
+                regions.Add(new IdRegion(usa.tok, OccurrenceKind.RecognizedAttributeId, null, usa.tok.val.Length));
+              }
+            }
+          }
+        }
+      }
+
+      private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ICallable callableContext, ModuleDefinition context) {
+        Contract.Requires(tok != null);
+        Contract.Requires(v != null);
+        Start = tok.pos;
+        Length = v.DisplayName.Length;
+        if (kind == null) {
+          // use default
+          if (v is LocalVariable) {
+            kind = "local variable";
+          } else if (v is BoundVar) {
+            kind = "bound variable";
+          } else {
+            var formal = (Formal)v;
+            kind = formal.InParam ? "in-parameter" : "out-parameter";
+            if (callableContext is TwoStateLemma && !formal.IsOld) {
+              kind = "new " + kind;
+            }
+            if (formal is ImplicitFormal) {
+              kind = "implicit " + kind;
+            }
+          }
+        }
+        Variable = v;
+        HoverText = string.Format("({2}{3}) {0}: {1}", v.DisplayName, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind);
+        Kind = !isDefinition ? OccurrenceKind.Use : LocalVariable.HasWildcardName(v) ? OccurrenceKind.WildDefinition : OccurrenceKind.Definition;
+      }
+      private IdRegion(Bpl.IToken tok, Field decl, Microsoft.Ivy.Type showType, string kind, bool isDefinition, ModuleDefinition context) {
+        Contract.Requires(tok != null);
+        Contract.Requires(decl != null);
+        Contract.Requires(kind != null);
+        if (showType == null) {
+          showType = decl.Type;
+        }
+        Start = tok.pos;
+        Length = decl.Name.Length;
+        HoverText = string.Format("({4}{2}{3}) {0}: {1}", decl.FullNameInContext(context), showType.TypeName(context),
+          decl.IsGhost ? "ghost " : "",
+          kind,
+          decl.IsUserMutable || decl is DatatypeDestructor ? "" : decl.IsMutable ? " non-assignable " : "immutable ");
+        Kind = !isDefinition ? OccurrenceKind.Use : OccurrenceKind.Definition;
+      }
+
+      private IdRegion(Bpl.IToken tok, OccurrenceKind occurrenceKind, string info, int length)
+      {
+        this.Start = tok.pos;
+        this.Length = length;
+        this.Kind = occurrenceKind;
+        this.HoverText = info;
+      }
+
+      /// <summary>
+      /// The following constructor is suitable for recognized attributes.
+      /// </summary>
+      private IdRegion(Bpl.IToken from, Bpl.IToken thru, OccurrenceKind occurrenceKind) {
+        this.Start = from.pos;
+        this.Length = thru.pos + thru.val.Length - from.pos;
+        this.Kind = occurrenceKind;
+        this.HoverText = null;
+      }
+    }
+  }
+
+  public abstract class IvyRegion
+  {
+    public static bool InMainFileAndUserDefined(Microsoft.Ivy.Program prog, Bpl.IToken tok) {
+      Contract.Requires(prog != null);
+      Contract.Requires(tok != null);
+      return object.Equals(prog.FullName, tok.filename) && !(tok is AutoGeneratedToken);
+    }
+  }
+
+  #endregion
+}
--- a/vs/ext/IvyExtension.csproj
+++ b/vs/ext/IvyExtension.csproj
@ -0,0 +1,188 @@
+<?xml version="1.0" encoding="utf-8"?>
+<Project DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003" ToolsVersion="4.0">
+  <PropertyGroup>
+    <MinimumVisualStudioVersion>14.0</MinimumVisualStudioVersion>
+    <VisualStudioVersion Condition="'$(VisualStudioVersion)' == ''">11.0</VisualStudioVersion>
+    <VSToolsPath Condition="'$(VSToolsPath)' == ''">$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion)</VSToolsPath>
+    <TargetFrameworkProfile />
+    <FileUpgradeFlags>
+    </FileUpgradeFlags>
+    <UpgradeBackupLocation>
+    </UpgradeBackupLocation>
+    <OldToolsVersion>4.0</OldToolsVersion>
+    <PublishUrl>publish\</PublishUrl>
+    <Install>true</Install>
+    <InstallFrom>Disk</InstallFrom>
+    <UpdateEnabled>false</UpdateEnabled>
+    <UpdateMode>Foreground</UpdateMode>
+    <UpdateInterval>7</UpdateInterval>
+    <UpdateIntervalUnits>Days</UpdateIntervalUnits>
+    <UpdatePeriodically>false</UpdatePeriodically>
+    <UpdateRequired>false</UpdateRequired>
+    <MapFileExtensions>true</MapFileExtensions>
+    <ApplicationRevision>0</ApplicationRevision>
+    <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
+    <IsWebBootstrapper>false</IsWebBootstrapper>
+    <UseApplicationTrust>false</UseApplicationTrust>
+    <BootstrapperEnabled>true</BootstrapperEnabled>
+    <StartAction>Program</StartAction>
+    <StartProgram>$(DevEnvDir)\devenv.exe</StartProgram>
+    <StartArguments>/rootsuffix Exp</StartArguments>
+  </PropertyGroup>
+  <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
+  <PropertyGroup>
+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+    <SchemaVersion>2.0</SchemaVersion>
+    <ProjectGuid>{6E9A5E14-0763-471C-A129-80A879D9E7BA}</ProjectGuid>
+    <ProjectTypeGuids>{82b43b9b-a64c-4715-b499-d71e9ca2bd60};{60dc8134-eba5-43b8-bcc9-bb4bc16c2548};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}</ProjectTypeGuids>
+    <OutputType>Library</OutputType>
+    <AppDesignerFolder>Properties</AppDesignerFolder>
+    <RootNamespace>DafnyLanguage</RootNamespace>
+    <AssemblyName>DafnyLanguageService</AssemblyName>
+    <SignAssembly>false</SignAssembly>
+    <AssemblyOriginatorKeyFile>
+    </AssemblyOriginatorKeyFile>
+    <TargetFrameworkVersion>v4.5</TargetFrameworkVersion>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+    <DebugSymbols>true</DebugSymbols>
+    <DebugType>full</DebugType>
+    <Optimize>false</Optimize>
+    <OutputPath>..\..\Binaries\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <ErrorReport>prompt</ErrorReport>
+    <WarningLevel>4</WarningLevel>
+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+    <Prefer32Bit>false</Prefer32Bit>
+    <PlatformTarget>AnyCPU</PlatformTarget>
+    <CreateVsixContainer>True</CreateVsixContainer>
+    <DeployExtension>True</DeployExtension>
+    <CopyVsixExtensionFiles>false</CopyVsixExtensionFiles>
+    <GeneratePkgDefFile>false</GeneratePkgDefFile>
+    <CopyVsixManifestToOutput>false</CopyVsixManifestToOutput>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+    <DebugType>pdbonly</DebugType>
+    <Optimize>true</Optimize>
+    <OutputPath>..\..\Binaries\</OutputPath>
+    <DefineConstants>TRACE</DefineConstants>
+    <ErrorReport>prompt</ErrorReport>
+    <WarningLevel>4</WarningLevel>
+    <RunCodeAnalysis>true</RunCodeAnalysis>
+    <Prefer32Bit>false</Prefer32Bit>
+  </PropertyGroup>
+  <ItemGroup>
+    <Reference Include="Microsoft.QualityTools.Testing.Fakes, Version=12.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+      <SpecificVersion>False</SpecificVersion>
+    </Reference>
+  </ItemGroup>
+  <ItemGroup>
+    <Reference Include="Microsoft.VisualStudio.ComponentModelHost, Version=14.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+    <Reference Include="Microsoft.VisualStudio.CoreUtility, Version=14.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+    <Reference Include="Microsoft.VisualStudio.Editor, Version=14.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+    <Reference Include="Microsoft.VisualStudio.Language.Intellisense, Version=14.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+    <Reference Include="Microsoft.VisualStudio.Language.StandardClassification, Version=14.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+    <Reference Include="Microsoft.VisualStudio.Shell.14.0, Version=14.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.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.Text.Data, Version=14.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+    <Reference Include="Microsoft.VisualStudio.Text.Logic, Version=14.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+    <Reference Include="Microsoft.VisualStudio.Text.UI, Version=14.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+    <Reference Include="Microsoft.VisualStudio.Text.UI.Wpf, Version=14.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+    <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>
+  </ItemGroup>
+  <ItemGroup>
+    <Reference Include="PresentationCore" />
+    <Reference Include="PresentationFramework" />
+    <Reference Include="System" />
+    <Reference Include="System.ComponentModel.Composition" />
+    <Reference Include="System.Core" />
+    <Reference Include="System.Xaml" />
+    <Reference Include="WindowsBase" />
+  </ItemGroup>
+  <ItemGroup>
+    <COMReference Include="EnvDTE">
+      <Guid>{80CC9F66-E7D8-4DDD-85B6-D9E6CD0E93E2}</Guid>
+      <VersionMajor>8</VersionMajor>
+      <VersionMinor>0</VersionMinor>
+      <Lcid>0</Lcid>
+      <WrapperTool>primary</WrapperTool>
+      <Isolated>False</Isolated>
+      <EmbedInteropTypes>False</EmbedInteropTypes>
+    </COMReference>
+  </ItemGroup>
+  <ItemGroup>
+    <Compile Include="BufferIdleEventUtil.cs" />
+    <Compile Include="GlobalSuppressions.cs" />
+    <Compile Include="HoverText.cs" />
+    <Compile Include="ContentType.cs" />
+    <Compile Include="BraceMatching.cs" />
+    <Compile Include="WordHighlighter.cs" />
+    <Compile Include="TokenTagger.cs" />
+    <Compile Include="ClassificationTagger.cs" />
+    <Compile Include="Properties\AssemblyInfo.cs" />
+  </ItemGroup>
+  <ItemGroup>
+    <Fakes Include="Fakes\Microsoft.VisualStudio.ComponentModelHost.fakes" />
+    <None Include="packages.config">
+      <SubType>Designer</SubType>
+    </None>
+    <None Include="source.extension.vsixmanifest">
+      <SubType>Designer</SubType>
+    </None>
+  </ItemGroup>
+  <ItemGroup>
+    <BootstrapperPackage Include=".NETFramework,Version=v4.5">
+      <Visible>False</Visible>
+      <ProductName>Microsoft .NET Framework 4.5 %28x86 and x64%29</ProductName>
+      <Install>true</Install>
+    </BootstrapperPackage>
+    <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
+      <Visible>False</Visible>
+      <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
+      <Install>false</Install>
+    </BootstrapperPackage>
+    <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
+      <Visible>False</Visible>
+      <ProductName>.NET Framework 3.5 SP1</ProductName>
+      <Install>false</Install>
+    </BootstrapperPackage>
+  </ItemGroup>
+  <ItemGroup>
+    <WCFMetadata Include="Service References\" />
+  </ItemGroup>
+  <PropertyGroup>
+    <UseCodebase>true</UseCodebase>
+  </PropertyGroup>
+  <Import Project="$(MSBuildBinPath)\Microsoft.CSharp.targets" />
+  <Import Project="$(VSToolsPath)\VSSDK\Microsoft.VsSDK.targets" Condition="'$(VSToolsPath)' != ''" />
+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
+       Other similar extension points exist, see Microsoft.Common.targets.
+  <Target Name="BeforeBuild">
+  </Target>
+  <Target Name="AfterBuild">
+  </Target>
+  -->
+</Project>
--- a/vs/ext/IvyExtension.sln
+++ b/vs/ext/IvyExtension.sln
@ -0,0 +1,22 @@
+
+Microsoft Visual Studio Solution File, Format Version 12.00
+# Visual Studio 14
+VisualStudioVersion = 14.0.25420.1
+MinimumVisualStudioVersion = 10.0.40219.1
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "IvyExtension", "IvyExtension.csproj", "{6E9A5E14-0763-471C-A129-80A879D9E7BA}"
+EndProject
+Global
+	GlobalSection(SolutionConfigurationPlatforms) = preSolution
+		Debug|Any CPU = Debug|Any CPU
+		Release|Any CPU = Release|Any CPU
+	EndGlobalSection
+	GlobalSection(ProjectConfigurationPlatforms) = postSolution
+		{6E9A5E14-0763-471C-A129-80A879D9E7BA}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{6E9A5E14-0763-471C-A129-80A879D9E7BA}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{6E9A5E14-0763-471C-A129-80A879D9E7BA}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{6E9A5E14-0763-471C-A129-80A879D9E7BA}.Release|Any CPU.Build.0 = Release|Any CPU
+	EndGlobalSection
+	GlobalSection(SolutionProperties) = preSolution
+		HideSolutionNode = FALSE
+	EndGlobalSection
+EndGlobal
--- a/vs/ext/KeyBindingFilter.cs
+++ b/vs/ext/KeyBindingFilter.cs
@ -0,0 +1,146 @@
+using System;
+using System.ComponentModel.Composition;
+using EnvDTE;
+using Microsoft.VisualStudio;
+using Microsoft.VisualStudio.OLE.Interop;
+using Microsoft.VisualStudio.Utilities;
+using Microsoft.VisualStudio.Editor;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.TextManager.Interop;
+using Microsoft.VisualStudio.Shell;
+using Microsoft.VisualStudio.Shell.Interop;
+
+namespace DafnyLanguage
+{
+  internal class KeyBindingCommandFilter : IOleCommandTarget
+  {
+    private IWpfTextView m_textView;
+    internal IOleCommandTarget m_nextTarget;
+    internal bool m_added;
+
+    [Import(typeof(Microsoft.VisualStudio.Shell.SVsServiceProvider))]
+    internal System.IServiceProvider _serviceProvider = null;
+
+    public KeyBindingCommandFilter(IWpfTextView textView) {
+      m_textView = textView;
+    }
+
+
+    public int QueryStatus(ref Guid pguidCmdGroup, uint cCmds, OLECMD[] prgCmds, IntPtr pCmdText) {
+      if (pguidCmdGroup == typeof(VSConstants.VSStd97CmdID).GUID) {
+        if (cCmds == 1) {
+          switch (prgCmds[0].cmdID) {
+            case (uint)VSConstants.VSStd97CmdID.GotoDefn: // F12
+            case (uint)VSConstants.VSStd97CmdID.Start:    // F5
+            case (uint)VSConstants.VSStd97CmdID.StepInto: // F11 
+              prgCmds[0].cmdf = (uint) OLECMDF.OLECMDF_SUPPORTED;
+              prgCmds[0].cmdf |= (uint)OLECMDF.OLECMDF_ENABLED;
+              return VSConstants.S_OK;
+          }
+        }
+      }
+      return m_nextTarget.QueryStatus(ref pguidCmdGroup, cCmds, prgCmds, pCmdText);
+    }
+
+    public int Exec(ref Guid pguidCmdGroup, uint nCmdID, uint nCmdexecopt, IntPtr pvaIn, IntPtr pvaOut) {
+      if (pguidCmdGroup == typeof(VSConstants.VSStd97CmdID).GUID) {
+        switch (nCmdID) {
+          case (uint)VSConstants.VSStd97CmdID.Start:    // F5
+            if (DafnyClassifier.DafnyMenuPackage.MenuProxy.StopVerifierCommandEnabled(m_textView)) {
+              DafnyClassifier.DafnyMenuPackage.MenuProxy.StopVerifier(m_textView);
+            } else {
+              DafnyClassifier.DafnyMenuPackage.MenuProxy.RunVerifier(m_textView);
+            }
+            return VSConstants.S_OK;
+          case (uint)VSConstants.VSStd97CmdID.StepInto:
+            if (DafnyClassifier.DafnyMenuPackage.MenuProxy.StopResolverCommandEnabled(m_textView)) {
+              DafnyClassifier.DafnyMenuPackage.MenuProxy.StopResolver(m_textView);
+            } else {
+              DafnyClassifier.DafnyMenuPackage.MenuProxy.RunResolver(m_textView);
+            }
+            return VSConstants.S_OK;
+          case (uint)VSConstants.VSStd97CmdID.GotoDefn: // F12
+            DafnyClassifier.DafnyMenuPackage.MenuProxy.GoToDefinition(m_textView);
+            return VSConstants.S_OK;
+        }
+      }
+
+      return m_nextTarget.Exec(pguidCmdGroup, nCmdID, nCmdexecopt, pvaIn, pvaOut);
+    }
+  }
+
+  [Export(typeof(IVsTextViewCreationListener))]
+  [ContentType("dafny")]
+  [TextViewRole(PredefinedTextViewRoles.Editable)]
+  internal class KeyBindingCommandFilterProvider : IVsTextViewCreationListener {
+
+    [Import(typeof(IVsEditorAdaptersFactoryService))]
+    internal IVsEditorAdaptersFactoryService editorFactory = null;
+    Events events;
+    EnvDTE.DocumentEvents documentEvents;
+
+
+    public void VsTextViewCreated(IVsTextView textViewAdapter) {
+      IWpfTextView textView = editorFactory.GetWpfTextView(textViewAdapter);
+      if (textView == null)
+        return;
+
+      AddCommandFilter(textViewAdapter, new KeyBindingCommandFilter(textView));
+
+      // add Document saved event
+      DTE dte = (DTE)ServiceProvider.GlobalProvider.GetService(typeof(DTE));
+      events = (Events)dte.Events;
+      documentEvents = events.DocumentEvents;
+      documentEvents.DocumentSaved += DocumentSaved;
+    }
+
+    private void DocumentSaved(EnvDTE.Document document) {
+      DafnyLanguage.ProgressTagger tagger;
+      IWpfTextView textView = GetWpfTextView(document.FullName);
+      if (textView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(textView.TextBuffer, out tagger)) {
+        MenuProxy.Output("restart verifier on file save: " + document.FullName + "\n");
+        // stop the old verification
+        tagger.StopVerification();
+
+        // start a new one.
+        tagger.StartVerification(false);
+      }
+    }
+
+    private IWpfTextView GetWpfTextView(string filePath) {
+      DTE dte = (DTE)ServiceProvider.GlobalProvider.GetService(typeof(DTE));
+      Microsoft.VisualStudio.OLE.Interop.IServiceProvider provider = (Microsoft.VisualStudio.OLE.Interop.IServiceProvider)dte;
+      ServiceProvider serviceProvider = new ServiceProvider(provider);
+
+      IVsUIHierarchy uiHierarchy;
+      uint itemID;
+      IVsWindowFrame windowFrame;
+      
+      if (Microsoft.VisualStudio.Shell.VsShellUtilities.IsDocumentOpen(serviceProvider, filePath, Guid.Empty,
+                                      out uiHierarchy, out itemID, out windowFrame)) {
+        // Get the IVsTextView from the windowFrame.
+        IVsTextView textView =  Microsoft.VisualStudio.Shell.VsShellUtilities.GetTextView(windowFrame);
+        return editorFactory.GetWpfTextView(textView);
+      }
+
+      return null;
+    }
+
+
+    void AddCommandFilter(IVsTextView viewAdapter, KeyBindingCommandFilter commandFilter) {
+      if (commandFilter.m_added == false) {
+        //get the view adapter from the editor factory
+        IOleCommandTarget next;
+        int hr = viewAdapter.AddCommandFilter(commandFilter, out next);
+
+        if (hr == VSConstants.S_OK) {
+          commandFilter.m_added = true;
+          //you'll need the next target for Exec and QueryStatus 
+          if (next != null)
+            commandFilter.m_nextTarget = next;
+        }
+      }
+    }
+
+  }
+}
--- a/vs/ext/MenuProxy.cs
+++ b/vs/ext/MenuProxy.cs
@ -0,0 +1,220 @@
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Shell;
+using Microsoft.VisualStudio.Shell.Interop;
+
+namespace DafnyLanguage
+{
+  class MenuProxy : DafnyLanguage.DafnyMenu.IMenuProxy
+  {
+    private DafnyMenu.DafnyMenuPackage DafnyMenuPackage;
+
+    public MenuProxy(DafnyMenu.DafnyMenuPackage DafnyMenuPackage)
+    {
+      this.DafnyMenuPackage = DafnyMenuPackage;
+    }
+
+    public int ToggleSnapshotVerification(IWpfTextView activeTextView)
+    {
+      return DafnyDriver.ChangeIncrementalVerification(1);
+    }
+
+    public int ToggleMoreAdvancedSnapshotVerification(IWpfTextView activeTextView)
+    {
+      return DafnyDriver.ChangeIncrementalVerification(2);
+    }
+
+    public bool MoreAdvancedSnapshotVerificationCommandEnabled(IWpfTextView activeTextView)
+    {
+      return activeTextView != null
+             && 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;
+      return activeTextView != null
+                    && StopResolverCommandEnabled(activeTextView) // verifier can start/stop only when resolver is running.
+                    && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger)
+                    && tagger != null && !tagger.VerificationDisabled;
+    }
+
+    public void StopVerifier(IWpfTextView activeTextView)
+    {
+      DafnyLanguage.ProgressTagger tagger;
+      if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger))
+      {
+        MenuProxy.Output("verifier manually stopped\n");
+        tagger.StopVerification();
+      }
+    }
+
+    public bool RunVerifierCommandEnabled(IWpfTextView activeTextView)
+    {
+      DafnyLanguage.ProgressTagger tagger;
+      return activeTextView != null
+                 && StopResolverCommandEnabled(activeTextView) // verifier can start/stop only when resolver is running.       
+                 && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger)
+                 && tagger != null && tagger.VerificationDisabled;
+    }
+
+    public void RunVerifier(IWpfTextView activeTextView)
+    {
+      DafnyLanguage.ProgressTagger tagger;
+      if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger))
+      {
+        MenuProxy.Output("verifier manually started\n");
+        tagger.StartVerification(false);
+      }
+    }
+
+    public bool StopResolverCommandEnabled(IWpfTextView activeTextView) {
+      DafnyLanguage.ResolverTagger resolver;
+      return activeTextView != null
+                    && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
+                    && resolver != null && resolver.RunResolver;
+    }
+
+    public void StopResolver(IWpfTextView activeTextView) {
+      DafnyLanguage.ResolverTagger resolver;
+      if (activeTextView != null && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)) {
+        MenuProxy.Output("resolver and verifier manually stopped\n");
+        resolver.RunResolver = false;
+        resolver.Program = null;
+      }
+      DafnyLanguage.ProgressTagger tagger;
+      if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger)) {
+        tagger.StartVerification(false);
+      }
+    }
+
+    public bool RunResolverCommandEnabled(IWpfTextView activeTextView) {
+      DafnyLanguage.ResolverTagger resolver;
+      return activeTextView != null
+                 && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
+                 && resolver != null && !resolver.RunResolver;
+    }
+
+    public void RunResolver(IWpfTextView activeTextView) {
+      DafnyLanguage.ResolverTagger resolver;
+      if (activeTextView != null && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)) {
+        MenuProxy.Output("resolver and verifier manually started\n");
+        resolver.RunResolver = true;
+        resolver.ResolveBuffer(null, null);
+      }
+      DafnyLanguage.ProgressTagger tagger;
+      if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger)) {
+        tagger.StartVerification(false);
+      }
+    }
+
+    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";
+    }
+
+    public bool CompileCommandEnabled(IWpfTextView activeTextView)
+    {
+      ResolverTagger resolver;
+      return activeTextView != null
+                    && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
+                    && 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;
+      if (activeTextView != null
+          && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
+          && resolver.Program != null)
+      {
+        var outputWriter = new StringWriter();
+        DafnyMenuPackage.ExecuteAsCompiling(() => { DafnyDriver.Compile(resolver.Program, outputWriter); }, outputWriter);
+      }
+    }
+
+    public bool ShowErrorModelCommandEnabled(IWpfTextView activeTextView)
+    {
+      ResolverTagger resolver;
+      return activeTextView != null
+                    && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
+                    && resolver.Program != null
+                    && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.ModelText));
+    }
+
+    public void ShowErrorModel(IWpfTextView activeTextView)
+    {
+      ResolverTagger resolver = null;
+      var show = activeTextView != null
+                 && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
+                 && resolver.Program != null
+                 && resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.ModelText));
+      if (show)
+      {
+        var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.ModelText));
+
+        if (selectedError != null)
+        {
+          DafnyMenuPackage.ShowErrorModelInBVD(selectedError.ModelText, selectedError.SelectedStateId);
+        }
+      }
+    }
+
+    public void GoToDefinition(IWpfTextView activeTextView) {
+      int caretPos = activeTextView.Caret.Position.BufferPosition.Position;
+      string fileName;
+      int lineNumber;
+      int offset;
+      DafnyLanguage.IdentifierTagger tagger;
+      if (activeTextView != null && DafnyLanguage.IdentifierTagger.IdentifierTaggers.TryGetValue(activeTextView.TextBuffer, out tagger)) {
+        if (tagger.FindDefinition(caretPos, out fileName, out lineNumber, out offset)) {
+          DafnyMenuPackage.GoToDefinition(fileName, lineNumber, offset);
+        }
+      }
+    }
+
+    public static void Output(string msg) {
+      // Get the output window
+      var outputWindow = Package.GetGlobalService(typeof(SVsOutputWindow)) as IVsOutputWindow;
+
+      // Ensure that the desired pane is visible
+      var paneGuid = Microsoft.VisualStudio.VSConstants.OutputWindowPaneGuid.GeneralPane_guid;
+      IVsOutputWindowPane pane;
+      outputWindow.CreatePane(paneGuid, "Dafny", 1, 0);
+      outputWindow.GetPane(paneGuid, out pane);
+
+      // Output the message
+      pane.OutputString(msg);
+    }
+  }
+}
--- a/vs/ext/OutliningTagger.cs
+++ b/vs/ext/OutliningTagger.cs
@ -0,0 +1,217 @@
+using System;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using System.Diagnostics.Contracts;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+using Bpl = Microsoft.Boogie;
+using Dafny = Microsoft.Dafny;
+
+
+namespace DafnyLanguage
+{
+
+  #region Provider
+
+  [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<IDafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<IDafnyResolverTag>(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);
+    }
+  }
+
+  #endregion
+
+
+  #region Tagger
+
+  /// <summary>
+  /// Translate DafnyResolverTag's into IOutliningRegionTag's
+  /// </summary>
+  internal sealed class OutliningTagger : ITagger<IOutliningRegionTag>
+  {
+    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<OutliningRegion> _regions = new List<OutliningRegion>();  // the regions generated from _program
+    ITagAggregator<IDafnyResolverTag> _aggregator;
+
+    internal OutliningTagger(ITextBuffer buffer, ITagAggregator<IDafnyResolverTag> tagAggregator) {
+      _buffer = buffer;
+      _snapshot = _buffer.CurrentSnapshot;
+      _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;
+      // (A NormalizedSnapshotSpanCollection contains spans that all come from the same snapshot.)
+      // The spans are ordered by the .Start component, and the collection contains no adjacent or abutting spans.
+      // Hence, to find a span that includes all the ones in "spans", we only need to look at the .Start for the
+      // first spand and the .End of the last span:
+      var startPoint = spans[0].Start;
+      var endPoint = spans[spans.Count - 1].End;
+
+      // Note, (startPoint,endPoint) are points in the spans for which we're being asked to provide tags.  We need to translate
+      // these back into the most recent snapshot that we've computed regions for, namely _snapshot.
+      var entire = new SnapshotSpan(startPoint, endPoint).TranslateTo(_snapshot, SpanTrackingMode.EdgeExclusive);
+      int start = entire.Start;
+      int end = entire.End;
+      if (start == end) yield break;
+
+      foreach (var r in _regions) {
+        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));
+        }
+      }
+    }
+
+    // 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) {
+        ITextSnapshot snap;
+        Microsoft.Dafny.Program prog;
+        lock (this) {
+          snap = r.Snapshot;
+          prog = r.Program;
+        }
+        if (prog != null) {
+          if (!ComputeOutliningRegions(prog, snap))
+            return;  // no new regions
+
+          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));
+            }
+          }
+        }
+      }
+    }
+
+    bool ComputeOutliningRegions(Dafny.Program program, ITextSnapshot snapshot) {
+      Contract.Requires(snapshot != null);
+
+      if (program == _program)
+        return false;  // no new regions
+
+      List<OutliningRegion> newRegions = new List<OutliningRegion>();
+
+      foreach (var module in program.Modules()) {
+        if (!module.IsDefaultModule) {
+          var nm = "module";
+          if (module.IsAbstract) {
+            nm = "abstract " + 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) {
+            OutliningRegion.Add(newRegions, program, d, "type");
+          } else if (d is Dafny.CoDatatypeDecl) {
+            OutliningRegion.Add(newRegions, program, d, "codatatype");
+          } else if (d is Dafny.DatatypeDecl) {
+            OutliningRegion.Add(newRegions, program, d, "datatype");
+          } else if (d is Dafny.ModuleDecl) {
+            // do nothing here, since the outer loop handles modules
+          } else {
+            var cl = (Dafny.ClassDecl)d;
+            if (cl.IsDefaultClass) {
+              // do nothing
+            } else if (cl is Dafny.IteratorDecl) {
+              OutliningRegion.Add(newRegions, program, cl, "iterator");
+            } else {
+              OutliningRegion.Add(newRegions, program, cl, "class");
+            }
+            // do the class members (in particular, functions and methods)
+            foreach (Dafny.MemberDecl m in cl.Members) {
+              if (!HasBodyTokens(m)) {
+                continue;
+              }
+              if (m is Dafny.Function && ((Dafny.Function)m).Body != null) {
+                var nm =
+                  m is Dafny.InductivePredicate ? "inductive predicate" :
+                  m is Dafny.CoPredicate ? "copredicate" :
+                  // m is Dafny.PrefixPredicate ? "prefix predicate" :  // this won't ever occur here
+                  m is Dafny.Predicate ? "predicate" :
+                  "function";
+                if (!m.IsGhost) {
+                  nm += " method";
+                }
+                OutliningRegion.Add(newRegions, program, m, nm);
+              } else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) {
+                var nm =
+                  m is Dafny.Constructor ? "constructor" :
+                  m is Dafny.CoLemma ? "colemma" :
+                  m is Dafny.Lemma ? "lemma" :
+                  // m is Dafny.PrefixLemma ? "prefix lemma" :  // this won't ever occur here
+                  "method";
+                if (m.IsGhost && !(m is Dafny.CoLemma)) {
+                  nm = "ghost " + nm;
+                }
+                OutliningRegion.Add(newRegions, program, m, nm);
+              }
+            }
+          }
+        }
+      }
+      _snapshot = snapshot;
+      _regions = newRegions;
+      _program = program;
+      return true;
+    }
+
+    static bool HasBodyTokens(Dafny.Declaration decl) {
+      Contract.Requires(decl != null);
+      return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken;
+    }
+
+    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;
+      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;
+        Length = length;
+        HoverText = string.Format("body of {0} {1}", kind, decl.Name);
+      }
+    }
+  }
+
+  #endregion
+
+}
--- a/vs/ext/ProgressMargin.cs
+++ b/vs/ext/ProgressMargin.cs
@ -0,0 +1,467 @@
+using System;
+using System.Collections.Concurrent;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using System.Diagnostics.Contracts;
+using System.IO;
+using System.Linq;
+using System.Text.RegularExpressions;
+using System.Threading;
+using System.Threading.Tasks;
+using System.Windows;
+using System.Windows.Media;
+using System.Windows.Shapes;
+using System.Windows.Threading;
+using Microsoft.VisualStudio.Shell;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Formatting;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+using Dafny = Microsoft.Dafny;
+
+
+namespace DafnyLanguage
+{
+
+  #region UI stuff
+
+  internal class ProgressMarginGlyphFactory : IGlyphFactory
+  {
+    public UIElement GenerateGlyph(IWpfTextViewLine line, IGlyphTag tag) {
+      var pgt = tag as ProgressGlyphTag;
+      if (pgt == null) {
+        return null;
+      }
+
+      return new Rectangle()
+      {
+        Fill = pgt.Val == 0 ? Brushes.Violet : Brushes.DarkOrange,
+        Height = 18.0,
+        Width = 3.0
+      };
+    }
+  }
+
+  [Export(typeof(IGlyphFactoryProvider))]
+  [Name("ProgressMarginGlyph")]
+  [Order(After = "TokenTagger")]
+  [ContentType("dafny")]
+  [TagType(typeof(ProgressGlyphTag))]
+  internal sealed class ProgressMarginGlyphFactoryProvider : IGlyphFactoryProvider
+  {
+    public IGlyphFactory GetGlyphFactory(IWpfTextView view, IWpfTextViewMargin margin) {
+      return new ProgressMarginGlyphFactory();
+    }
+  }
+
+  internal class ProgressGlyphTag : IGlyphTag
+  {
+    public readonly int Val;
+    public ProgressGlyphTag(int val) {
+      Val = val;
+    }
+  }
+
+  internal class RunVerifierThreadParams
+  {
+    public RunVerifierThreadParams(Dafny.Program i_program, ITextSnapshot i_snapshot, string i_requestId, ResolverTagger i_errorListHolder, bool i_diagnoseTimeouts)
+    {
+      program = i_program;
+      snapshot = i_snapshot;
+      requestId = i_requestId;
+      errorListHolder = i_errorListHolder;
+      diagnoseTimeouts = i_diagnoseTimeouts;
+    }
+
+    public Dafny.Program program;
+    public ITextSnapshot snapshot;
+    public string requestId;
+    public ResolverTagger errorListHolder;
+    public bool diagnoseTimeouts;
+  }
+
+  #endregion
+
+
+  #region Provider
+
+  [Export(typeof(ITaggerProvider))]
+  [ContentType("dafny")]
+  [Name("ProgressTagger")]
+  [TagType(typeof(ProgressGlyphTag))]
+  class ProgressTaggerProvider : ITaggerProvider
+  {
+    [Import]
+    internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
+
+    [Import(typeof(Microsoft.VisualStudio.Shell.SVsServiceProvider))]
+    internal IServiceProvider _serviceProvider = null;
+
+    [Import]
+    ITextDocumentFactoryService _textDocumentFactory = null;
+
+    public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+      ITagAggregator<IDafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<IDafnyResolverTag>(buffer);
+      // create a single tagger for each buffer.
+      Func<ITagger<T>> sc = delegate() { return new ProgressTagger(buffer, _serviceProvider, tagAggregator, _textDocumentFactory) as ITagger<T>; };
+      return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
+    }
+  }
+
+  #endregion
+
+
+  #region Tagger
+
+  public class ProgressTagger : ITagger<ProgressGlyphTag>, IDisposable
+  {
+    ErrorListProvider _errorProvider;
+    ITextBuffer _buffer;
+    ITextDocument _document;
+    bool _disposed;
+    bool _logSnapshots = false;
+    DateTime _created;
+    int _version;
+    int _verificationTaskStackSize = 16 * 1024 * 1024;
+
+    readonly DispatcherTimer timer;
+
+    public ProgressTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITagAggregator<IDafnyResolverTag> tagAggregator, ITextDocumentFactoryService textDocumentFactory) {
+      _buffer = buffer;
+
+      if (!textDocumentFactory.TryGetTextDocument(_buffer, out _document))
+      {
+        _document = null;
+      }
+
+      _errorProvider = new ErrorListProvider(serviceProvider);
+
+      timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle);
+      timer.Interval = TimeSpan.FromMilliseconds(50);
+      timer.Tick += new EventHandler(UponIdle);
+
+      tagAggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
+      buffer.Changed += new EventHandler<TextContentChangedEventArgs>(buffer_Changed);
+      bufferChangesPostVerificationStart.Add(new SnapshotSpan(buffer.CurrentSnapshot, 0, buffer.CurrentSnapshot.Length));
+      _created = DateTime.UtcNow;
+    }
+
+    public void Dispose()
+    {
+      Dispose(true);
+      GC.SuppressFinalize(this);
+    }
+
+    private void Dispose(bool disposing)
+    {
+      lock (this)
+      {
+        if (!_disposed)
+        {
+          if (disposing)
+          {
+            if (lastRequestId != null)
+            {
+              Microsoft.Boogie.ExecutionEngine.CancelRequest(lastRequestId);
+            }
+            if (_document != null && _document.TextBuffer != null)
+            {
+              ProgressTaggers.Remove(_document.TextBuffer);
+            }
+            _buffer.Changed -= buffer_Changed;
+            timer.Tick -= UponIdle;
+            _errorProvider.Dispose();
+            _errorProvider = null;
+            ClearCachedVerificationResults();
+            if (resolver != null)
+            {
+              resolver.Dispose();
+              resolver = null;
+            }
+          }
+
+          _disposed = true;
+        }
+      }
+    }
+
+    // The following fields and the contents of the following two lists are protected by the lock "this".
+    List<SnapshotSpan> bufferChangesPreVerificationStart = new List<SnapshotSpan>();  // buffer changes after the last completed verification and before the currently running verification
+    List<SnapshotSpan> bufferChangesPostVerificationStart = new List<SnapshotSpan>();  // buffer changes since the start of the currently running verification
+
+    void buffer_Changed(object sender, TextContentChangedEventArgs e) {
+      lock (this) {
+        foreach (var change in e.Changes) {
+          var startLine = e.After.GetLineFromPosition(change.NewPosition);
+          var endLine = e.After.GetLineFromPosition(change.NewEnd);
+          bufferChangesPostVerificationStart.Add(new SnapshotSpan(startLine.Start, endLine.End));
+        }
+      }
+    }
+
+    // The next field is protected by "this"
+    ResolverTagger resolver;
+    // Keep track of the most recent resolution results.
+    void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {
+      var r = sender as ResolverTagger;
+      if (r != null) {
+        lock (this) {
+          resolver = r;
+        }
+        timer.Stop();
+        timer.Start();
+      }
+    }
+
+    bool verificationInProgress;  // this field is protected by "this".  Invariant:  !verificationInProgress ==> bufferChangesPreVerificationStart.Count == 0
+    public bool VerificationDisabled { get; private set; }
+    bool isDiagnosingTimeouts;
+    string lastRequestId;
+
+    public static readonly IDictionary<ITextBuffer, ProgressTagger> ProgressTaggers = new ConcurrentDictionary<ITextBuffer, ProgressTagger>();
+
+    public readonly ConcurrentDictionary<string, ITextSnapshot> RequestIdToSnapshot = new ConcurrentDictionary<string, ITextSnapshot>();
+
+    /// <summary>
+    /// This method is invoked when the user has been idle for a little while.
+    /// Note, "sender" and "args" are allowed to be passed in as null--they are not used by this method.
+    /// </summary>
+    public void UponIdle(object sender, EventArgs args) {
+      lock (this) {
+        if (verificationInProgress) {
+          // This UponIdle message came at an inopportune time--we've already kicked off a verification.
+          // Just back off.
+          resolver.UpdateErrorList(resolver.Snapshot);
+          return;
+        }
+
+        if (resolver == null) return;
+        
+        Dafny.Program prog;
+        ITextSnapshot snap;
+        lock (resolver) {
+          prog = resolver.Program;
+          snap = resolver.Snapshot;
+        }
+        if (prog == null || VerificationDisabled) return;
+        // We have a successfully resolved program to verify
+
+        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
+        lastRequestId = null;
+        lock (RequestIdToSnapshot)
+        {
+          do
+          {
+            lastRequestId = DateTime.UtcNow.Ticks.ToString();
+          } while (RequestIdToSnapshot.ContainsKey(lastRequestId));
+          RequestIdToSnapshot[lastRequestId] = snap;
+        }
+
+        if (_document != null)
+        {
+          ProgressTaggers[_document.TextBuffer] = this;
+        }
+
+        RunVerifierThreadParams verifierThreadParams = new RunVerifierThreadParams(prog, snap, lastRequestId, resolver, dt);
+        Thread thread = new Thread(RunVerifierThreadRoutine, _verificationTaskStackSize);
+        thread.Start(verifierThreadParams);
+
+        verificationInProgress = true;
+        if (dt)
+        {
+          isDiagnosingTimeouts = false;
+        }
+
+        // Change orange progress markers into yellow ones
+        Contract.Assert(bufferChangesPreVerificationStart.Count == 0);  // follows from monitor invariant
+        var empty = bufferChangesPreVerificationStart;
+        bufferChangesPreVerificationStart = bufferChangesPostVerificationStart;
+        bufferChangesPostVerificationStart = empty;
+
+        // Notify to-whom-it-may-concern about the changes we just made
+        NotifyAboutChangedTags(snap);
+      }
+    }
+
+    private void NotifyAboutChangedTags(ITextSnapshot snap)
+    {
+      var chng = TagsChanged;
+      if (chng != null)
+      {
+        chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snap, 0, snap.Length)));
+      }
+    }
+
+    public void StopVerification()
+    {
+      Microsoft.Boogie.ExecutionEngine.CancelRequest(lastRequestId);
+      lock (this)
+      {
+        bufferChangesPreVerificationStart.Clear();
+        bufferChangesPostVerificationStart.Clear();
+        bufferChangesPostVerificationStart.Add(new SnapshotSpan(_buffer.CurrentSnapshot, 0, _buffer.CurrentSnapshot.Length));
+        VerificationDisabled = true;
+        verificationInProgress = false;
+        NotifyAboutChangedTags(_buffer.CurrentSnapshot);
+      }
+    }
+
+    public void StartVerification(bool clearCache = true, bool diagnoseTimeouts = false)
+    {
+      lock (this)
+      {
+        bufferChangesPreVerificationStart.Clear();
+        bufferChangesPostVerificationStart.Clear();
+        bufferChangesPostVerificationStart.Add(new SnapshotSpan(_buffer.CurrentSnapshot, 0, _buffer.CurrentSnapshot.Length));
+        VerificationDisabled = false;
+        isDiagnosingTimeouts = diagnoseTimeouts;
+        if (clearCache)
+        {
+          ClearCachedVerificationResults();
+        }
+        NotifyAboutChangedTags(_buffer.CurrentSnapshot);
+      }
+    }
+
+    private void ClearCachedVerificationResults()
+    {
+      if (_document != null)
+      {
+        Microsoft.Boogie.ExecutionEngine.Cache.RemoveMatchingKeys(new Regex(string.Format(@"^{0}:", Regex.Escape(GetHashCode().ToString()))));
+      }
+    }
+
+    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);
+      Contract.Requires(errorListHolder != null);
+
+      if (_logSnapshots)
+      {
+        var logDirName = System.IO.Path.Combine(System.IO.Path.GetDirectoryName(program.FullName), "logs");
+        Directory.CreateDirectory(logDirName);
+        var logFileName = System.IO.Path.Combine(logDirName, System.IO.Path.GetFileName(System.IO.Path.ChangeExtension(program.FullName, string.Format("{0}.v{1}{2}", _created.Ticks, _version, System.IO.Path.GetExtension(program.FullName)))));        
+        using (var writer = new StreamWriter(logFileName))
+        {
+          snapshot.Write(writer);
+        }
+        _version++;
+      }
+
+      DafnyDriver.SetDiagnoseTimeouts(diagnoseTimeouts);
+
+      try
+      {
+        string filename = _document != null ? _document.FilePath : "<program>";
+        var driver = new DafnyDriver(_buffer, filename);
+        bool success = driver.Verify(program, errorListHolder, GetHashCode().ToString(), requestId, errorInfo =>
+        {
+          if (!_disposed)
+          {
+            errorInfo.BoogieErrorCode = null;
+            var isRecycled = false;
+            ITextSnapshot s = null;
+            if (errorInfo.OriginalRequestId != null)
+            {
+              isRecycled = errorInfo.OriginalRequestId != requestId;
+              RequestIdToSnapshot.TryGetValue(errorInfo.OriginalRequestId, out s);
+            }
+            if (s == null && errorInfo.RequestId != null)
+            {
+              RequestIdToSnapshot.TryGetValue(errorInfo.RequestId, out s);
+            }
+            if (s != null)
+            {
+              errorListHolder.AddError(new DafnyError(errorInfo.Tok.filename, errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.FullMsg, s, isRecycled, errorInfo.Model.ToString(), System.IO.Path.GetFullPath(_document.FilePath) == errorInfo.Tok.filename), errorInfo.ImplementationName, requestId);
+              foreach (var aux in errorInfo.Aux)
+              {
+                errorListHolder.AddError(new DafnyError(aux.Tok.filename, aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.FullMsg, s, isRecycled, null, System.IO.Path.GetFullPath(_document.FilePath) == aux.Tok.filename), errorInfo.ImplementationName, requestId);
+              }
+            }
+          }
+        });
+        if (!success)
+        {
+          foreach (var error in driver.Errors) {
+            errorListHolder.AddError(error, "$$program$$", requestId);
+          }
+        }
+      }
+      catch (Exception e)
+      {
+        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();
+        verificationInProgress = false;
+      }
+
+      errorListHolder.UpdateErrorList(snapshot);
+
+      // Notify to-whom-it-may-concern about the cleared pre-verification changes
+      NotifyAboutChangedTags(snapshot);
+
+      // If new changes took place since we started the verification, we may need to kick off another verification
+      // immediately.
+      UponIdle(null, null);
+    }
+
+    private void RunVerifierThreadRoutine(object o)
+    {
+        RunVerifierThreadParams p = (RunVerifierThreadParams)o;
+        RunVerifier(p.program, p.snapshot, p.requestId, p.errorListHolder, p.diagnoseTimeouts);
+    }
+
+    public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+    IEnumerable<ITagSpan<ProgressGlyphTag>> ITagger<ProgressGlyphTag>.GetTags(NormalizedSnapshotSpanCollection spans)
+    {
+      if (spans.Count == 0) yield break;
+      var targetSnapshot = spans[0].Snapshot;
+
+      List<SnapshotSpan> pre;
+      List<SnapshotSpan> post;
+      lock (this) {
+        pre = bufferChangesPreVerificationStart.ToList();
+        post = bufferChangesPostVerificationStart.ToList();
+      }
+
+      // 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)));
+      foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, chs)) {
+        yield return new TagSpan<ProgressGlyphTag>(span, new ProgressGlyphTag(0));
+      }
+      chs = new NormalizedSnapshotSpanCollection(post.Select(span => span.TranslateTo(targetSnapshot, SpanTrackingMode.EdgeExclusive)));
+      foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, chs)) {
+        yield return new TagSpan<ProgressGlyphTag>(span, new ProgressGlyphTag(1));
+      }
+    }
+  }
+
+  #endregion
+
+}
--- a/vs/ext/Properties/AssemblyInfo.cs
+++ b/vs/ext/Properties/AssemblyInfo.cs
@ -0,0 +1,19 @@
+using System.Reflection;
+using System.Runtime.InteropServices;
+
+// General Information about an assembly is controlled through the following 
+// set of attributes. Change these attribute values to modify the information
+// associated with an assembly.
+[assembly: AssemblyTitle("DafnyLanguageService")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("Microsoft Research")]
+[assembly: AssemblyProduct("DafnyLanguageService")]
+[assembly: AssemblyCopyright("")]
+[assembly: AssemblyTrademark("")]
+[assembly: AssemblyCulture("")]
+
+// Setting ComVisible to false makes the types in this assembly not visible 
+// to COM components.  If you need to access a type in this assembly from 
+// COM, set the ComVisible attribute to true on that type.
+[assembly: ComVisible(false)]
--- a/vs/ext/ResolverTagger.cs
+++ b/vs/ext/ResolverTagger.cs
@ -0,0 +1,603 @@
+using System;
+using System.Collections.Concurrent;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using System.Diagnostics.Contracts;
+using System.IO;
+using System.Linq;
+using System.Text.RegularExpressions;
+using System.Windows.Shapes;
+using Microsoft.VisualStudio;
+using Microsoft.VisualStudio.Shell;
+using Microsoft.VisualStudio.Shell.Interop;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.TextManager.Interop;
+using Microsoft.VisualStudio.Utilities;
+using Dafny = Microsoft.Dafny;
+
+
+namespace DafnyLanguage
+{
+
+  #region Provider
+
+  [Export(typeof(ITaggerProvider))]
+  [ContentType("dafny")]
+  [TagType(typeof(IDafnyResolverTag))]
+  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);
+    }
+  }
+
+  #endregion
+
+
+  #region Tagger
+
+  #region Tags
+
+  public interface IDafnyResolverTag : ITag
+  {
+  }
+
+  public class DafnyErrorResolverTag : ErrorTag, IDafnyResolverTag
+  {
+    public DafnyError Error { get; private set; }
+
+    public DafnyErrorResolverTag(DafnyError error)
+      : base(ConvertToErrorType(error), error.Message)
+    {
+      Error = error;
+    }
+
+    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:
+          return "syntax error";  // COLOR: red
+        case ErrorCategory.ResolveError:
+          return "compiler error";  // COLOR: blue
+        case ErrorCategory.ParseWarning:
+        case ErrorCategory.ResolveWarning:
+          return "compiler warning";  // COLOR: blue
+        case ErrorCategory.InternalError:
+        case ErrorCategory.VerificationError:
+          return "error";  // COLOR: red
+        case ErrorCategory.AuxInformation:
+          return "other error";  // COLOR: purple red
+        default:
+          Contract.Assert(false);
+          throw new InvalidOperationException();
+      }
+    }
+  }
+
+  public class DafnyErrorStateResolverTag : IDafnyResolverTag
+  {
+    public readonly DafnyError Error;
+    public readonly ITrackingSpan Span;
+    public readonly int Id;
+    public readonly string Description;
+    public DafnyErrorStateResolverTag(DafnyError error, ITrackingSpan span, int id, string description)
+    {
+      Error = error;
+      Span = span;
+      Id = id;
+      Description = description;
+    }
+  }
+
+  public class DafnySuccessResolverTag : IDafnyResolverTag
+  {
+    public readonly Dafny.Program Program;
+    public DafnySuccessResolverTag(Dafny.Program program)
+    {
+      Program = program;
+    }
+  }
+
+  #endregion
+
+
+  /// <summary>
+  /// Translate PkgDefTokenTags into ErrorTags and Error List items
+  /// </summary>
+  public sealed class ResolverTagger : ITagger<IDafnyResolverTag>, IDisposable
+  {
+    readonly ITextBuffer _buffer;
+    readonly ITextDocument _document;
+    ErrorListProvider _errorProvider;
+    private bool m_disposed;
+
+    // The 'Snapshot' and 'Program' fields should be updated and read together, so they are protected by "this"
+    public ITextSnapshot Snapshot;  // may be null
+    public Dafny.Program Program;  // non-null only if the snapshot contains a Dafny program that type checks
+    public bool RunResolver { get; set; }  // whether the resolver should be run
+
+    List<DafnyError> _resolutionErrors = new List<DafnyError>();  // if nonempty, then _snapshot is the snapshot from which the errors were produced
+
+    internal void AddError(DafnyError error, string unitId, string requestId)
+    {
+      ErrorContainer entry;
+      if (_verificationErrors.TryGetValue(unitId, out entry))
+      {
+        lock (entry)
+        {
+          if (entry.RequestId == null || new DateTime(long.Parse(entry.RequestId)) < new DateTime(long.Parse(requestId)))
+          {
+            entry.Errors.Clear();
+            entry.RequestId = requestId;
+          }
+        }
+        entry.Errors.Push(error);
+        UpdateErrorList(Snapshot);
+      }
+    }
+
+    string MostRecentRequestId;
+    
+    internal void ReInitializeVerificationErrors(string mostRecentRequestId, IEnumerable<Microsoft.Boogie.Implementation> implementations)
+    {
+      var implNames = implementations.Select(impl => impl.Name);
+      lock (this)
+      {
+        MostRecentRequestId = mostRecentRequestId;
+        var outOfDatekeys = _verificationErrors.Keys.Except(implNames);
+        foreach (var key in outOfDatekeys)
+        {
+          ErrorContainer oldError;
+          _verificationErrors.TryRemove(key, out oldError);
+        }
+
+        var newKeys = implNames.Except(_verificationErrors.Keys).ToList();
+        newKeys.Add("$$program$$");
+        foreach (var key in newKeys)
+        {
+          _verificationErrors.TryAdd(key, new ErrorContainer());
+        }
+      }
+    }
+
+    public class ErrorContainer
+    {
+      internal string RequestId;
+      internal ConcurrentStack<DafnyError> Errors = new ConcurrentStack<DafnyError>();
+    }
+
+    public readonly ConcurrentDictionary<string, ErrorContainer> _verificationErrors = new ConcurrentDictionary<string, ErrorContainer>();
+
+    public IEnumerable<DafnyError> VerificationErrors
+    {
+      get
+      {
+        return _verificationErrors.Values.Where(ec => ec.RequestId == MostRecentRequestId).SelectMany(ec => ec.Errors.Reverse()).ToList();
+      }
+    }
+
+    public IEnumerable<DafnyError> AllErrors
+    {
+      get
+      {
+        lock (this)
+        {
+          bool anyResolutionErrors = false;
+          if (_resolutionErrors != null) {
+            foreach (var err in _resolutionErrors) {
+              if (CategoryConversion(err.Category) == TaskErrorCategory.Error) {
+                anyResolutionErrors = true;
+              }
+              yield return err;
+            }
+          }
+          if (!anyResolutionErrors) {
+            foreach (var err in VerificationErrors) {
+              yield return err;
+            }
+          }
+        }
+      }
+    }
+
+    public static readonly IDictionary<ITextBuffer, ResolverTagger> ResolverTaggers = new ConcurrentDictionary<ITextBuffer, ResolverTagger>();
+
+    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, ResolveBuffer);
+      this.RunResolver = true;
+    }
+
+    public void Dispose()
+    {
+      Dispose(true);
+      GC.SuppressFinalize(this);
+    }
+
+    private void Dispose(bool disposing)
+    {
+      lock (this)
+      {
+        if (!m_disposed)
+        {
+          if (disposing)
+          {
+            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();
+              _errorProvider = null;
+            }
+            BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer);
+            if (_document != null && _document.TextBuffer != null)
+            {
+              ResolverTaggers.Remove(_document.TextBuffer);
+            }
+          }
+
+          m_disposed = true;
+        }
+      }
+    }
+
+    /// <summary>
+    /// Find the Error tokens in the set of all tokens and create an ErrorTag for each
+    /// </summary>
+    public IEnumerable<ITagSpan<IDafnyResolverTag>> GetTags(NormalizedSnapshotSpanCollection spans)
+    {
+      if (spans.Count == 0) yield break;
+      var currentSnapshot = spans[0].Snapshot;
+      foreach (var err in AllErrors)
+      {
+        if (err.Category != ErrorCategory.ProcessError && err.Filename == System.IO.Path.GetFullPath(_document.FilePath))
+        {
+          yield return new TagSpan<IDafnyResolverTag>(err.Span.GetSpan(currentSnapshot), new DafnyErrorResolverTag(err));
+
+          if (err.StateSpans != null)
+          {
+            for (int i = 0; i < err.StateSpans.Length; i++)
+            {
+              var span = err.StateSpans[i];
+              var name = err.Model.States.ToArray()[i].Name;
+              var descStart = name.LastIndexOf(": ") + 2;
+              var description = 1 < descStart ? name.Substring(descStart) : "";
+              if (span != null)
+              {
+                yield return new TagSpan<IDafnyResolverTag>(span.GetSpan(currentSnapshot), new DafnyErrorStateResolverTag(err, span, i, description));
+              }
+            }
+          }
+        }
+      }
+
+      ITextSnapshot snap;
+      Dafny.Program prog;
+      lock (this)
+      {
+        snap = Snapshot;
+        prog = Program;
+      }
+      if (prog != null)
+      {
+        yield return new TagSpan<IDafnyResolverTag>(new SnapshotSpan(snap, 0, snap.Length), new DafnySuccessResolverTag(prog));
+      }
+    }
+
+    public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+    /// <summary>
+    /// Calls the Dafny parser/resolver/type checker on the contents of the buffer, updates the Error List accordingly.
+    /// </summary>
+    public 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(_buffer, filename);
+      List<DafnyError> newErrors;
+      Dafny.Program program;
+      try
+      {
+        program = driver.ProcessResolution(RunResolver);
+        newErrors = driver.Errors;
+      }
+      catch (Exception e)
+      {
+        newErrors = new List<DafnyError> { new DafnyError(filename, 0, 0, ErrorCategory.InternalError, "internal Dafny error: " + e.Message, snapshot, false) };
+        program = null;
+      }
+
+      lock (this)
+      {
+        Snapshot = snapshot;
+        Program = program;
+      }
+
+      if (program != null && _document != null)
+      {
+        ResolverTaggers[_document.TextBuffer] = this;
+      }
+      else if (_document != null)
+      {
+        ResolverTaggers.Remove(_document.TextBuffer);
+      }
+
+      _resolutionErrors = newErrors;
+
+      UpdateErrorList(snapshot);
+    }
+
+    public void UpdateErrorList(ITextSnapshot snapshot)
+    {
+      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.ResumeRefresh();
+      }
+      var chng = TagsChanged;
+      if (chng != null)
+        chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));
+    }
+
+    static TaskErrorCategory CategoryConversion(ErrorCategory cat)
+    {
+      switch (cat)
+      {
+        case ErrorCategory.ParseError:
+        case ErrorCategory.ResolveError:
+        case ErrorCategory.VerificationError:
+        case ErrorCategory.InternalError:
+          return TaskErrorCategory.Error;
+        case ErrorCategory.ParseWarning:
+        case ErrorCategory.ResolveWarning:
+          return TaskErrorCategory.Warning;
+        case ErrorCategory.AuxInformation:
+          return TaskErrorCategory.Message;
+        default:
+          Contract.Assert(false);  // unexpected category
+          return TaskErrorCategory.Error;  // please compiler
+      }
+    }
+
+    void NavigateHandler(object sender, EventArgs arguments)
+    {
+      var task = sender as ErrorTask;
+      if (task == null || task.Document == null)
+        return;
+
+      // This would have been the simple way of doing things:
+      //     _errorProvider.Navigate(error, new Guid(EnvDTE.Constants.vsViewKindCode));
+      // Unfortunately, it doesn't work--it seems to ignore the column position.  (Moreover, it wants 1-based
+      // line/column numbers, whereas the Error Task pane wants 0-based line/column numbers.)
+      // So, instead we do all the things that follow:
+
+      var openDoc = Package.GetGlobalService(typeof(IVsUIShellOpenDocument)) as IVsUIShellOpenDocument;
+      if (openDoc == null)
+        return;
+
+      IVsWindowFrame frame;
+      Microsoft.VisualStudio.OLE.Interop.IServiceProvider sp;
+      IVsUIHierarchy hier;
+      uint itemid;
+      Guid logicalView = VSConstants.LOGVIEWID_Code;
+      if (Microsoft.VisualStudio.ErrorHandler.Failed(openDoc.OpenDocumentViaProject(task.Document, ref logicalView, out sp, out hier, out itemid, out frame)) || frame == null)
+        return;
+
+      object docData;
+      Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(frame.GetProperty((int)__VSFPROPID.VSFPROPID_DocData, out docData));
+
+      // Get the VsTextBuffer
+      VsTextBuffer buffer = docData as VsTextBuffer;
+      if (buffer == null)
+      {
+        IVsTextBufferProvider bufferProvider = docData as IVsTextBufferProvider;
+        if (bufferProvider != null)
+        {
+          IVsTextLines lines;
+          Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(bufferProvider.GetTextBuffer(out lines));
+          buffer = lines as VsTextBuffer;
+          if (buffer == null)
+            return;
+        }
+      }
+
+      VsTextManager textManager = Package.GetGlobalService(typeof(VsTextManagerClass)) as VsTextManager;
+      if (textManager == null)
+        return;
+
+      // Finally, move the cursor
+      Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(textManager.NavigateToLineAndColumn(buffer, ref logicalView, task.Line, task.Column, task.Line, task.Column));
+    }
+  }
+
+
+  #region Errors
+
+  public enum ErrorCategory
+  {
+    ProcessError, ParseWarning, ParseError, ResolveWarning, ResolveError, VerificationError, AuxInformation, InternalError
+  }
+
+  public class DafnyError
+  {
+    public readonly string Filename;
+    public readonly int Line;  // 0 based
+    public readonly int Column;  // 0 based
+    public readonly ErrorCategory Category;
+    public readonly string Message;
+    protected readonly ITextSnapshot Snapshot;
+    public readonly ITrackingSpan Span;
+    public readonly string ModelText;
+    public Microsoft.Boogie.Model _model;
+    public Microsoft.Boogie.Model Model
+    {
+      get
+      {
+        if (_model == null && !string.IsNullOrEmpty(ModelText))
+        {
+          using (var rd = new StringReader(ModelText))
+          {
+            var models = Microsoft.Boogie.Model.ParseModels(rd).ToArray();
+            Contract.Assert(models.Length == 1);
+            _model = models[0];
+          }
+        }
+        return _model;
+      }
+    }
+    private ITrackingSpan[] _stateSpans;
+    public ITrackingSpan[] StateSpans
+    {
+      get
+      {
+        if (_stateSpans == null && Model != null)
+        {          
+          var model = Model;
+          var locRegex = new Regex(@"\((\d+),(\d+)\)");
+          _stateSpans = model.States.Select(
+           cs =>
+           {
+             var match = locRegex.Match(cs.Name);
+             if (!match.Success)
+             {
+               return null;
+             }
+             else
+             {
+               var line = Math.Max(0, int.Parse(match.Groups[1].Value) - 1);
+               var column = Math.Max(0, int.Parse(match.Groups[2].Value));
+               var sLine = Snapshot.GetLineFromLineNumber(line);
+               Contract.Assert(column <= sLine.Length);
+               var sLength = Math.Max(0, Math.Min(sLine.Length - column, 0));
+               return Snapshot.CreateTrackingSpan(sLine.Start + column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);
+             }
+           }).ToArray();
+        }
+        return _stateSpans;
+      }
+    }
+    public int SelectedStateId { get; set; }
+    public Shape SelectedStateAdornment { get; set; }
+    public bool IsSelected { get { return SelectedError == this; } }
+    private readonly ErrorSelection _errorSelection;
+    public DafnyError SelectedError { get { return _errorSelection.Error; } set { _errorSelection.Error = value; } }
+    public Shape Adornment;
+    public delegate void StateChangeEventHandler(object sender);
+    public event StateChangeEventHandler StateChangeEvent;
+    public void Notify()
+    {
+      if (StateChangeEvent != null)
+      {
+        StateChangeEvent(this);
+      }
+    }
+    public void UnsubscribeAll()
+    {
+      if (StateChangeEvent != null)
+      {
+        foreach (var d in StateChangeEvent.GetInvocationList())
+        {
+          StateChangeEvent -= (StateChangeEventHandler)d;
+        }
+      }
+    }
+
+    internal class ErrorSelection
+    {
+      internal DafnyError Error = null;
+    }
+
+    internal static readonly ErrorSelection _errorSelectionSingleton = new ErrorSelection();
+
+
+    /// <summary>
+    /// "line" and "col" are expected to be 0-based
+    /// </summary>
+    public DafnyError(string filename, int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot, bool isRecycled, string model = null, bool inCurrentDocument = true)
+    {
+      Filename = filename;
+      Line = Math.Max(0, line);
+      Column = Math.Max(0, col);
+      Category = cat;
+      Message = msg + ((isRecycled && cat == ErrorCategory.VerificationError) ? " (recycled)" : "");
+      Snapshot = snapshot;
+      if (inCurrentDocument) {
+        var sLine = snapshot.GetLineFromLineNumber(line);
+        Contract.Assert(Column <= sLine.Length);
+        var sLength = Math.Max(0, Math.Min(sLine.Length - Column, 5));
+        Span = snapshot.CreateTrackingSpan(sLine.Start + Column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);
+      } else {
+        Span = null;
+      }
+      ModelText = model;
+      _errorSelection = _errorSelectionSingleton;
+      SelectedStateId = -1;
+    }
+  }
+
+  #endregion
+
+  #endregion
+
+}
--- a/vs/ext/TokenTagger.cs
+++ b/vs/ext/TokenTagger.cs
@ -0,0 +1,454 @@
+using System;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using System.Linq;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+using System.Diagnostics.Contracts;
+
+
+namespace IvyLanguage
+{
+
+  #region Provider
+
+  [Export(typeof(ITaggerProvider))]
+  [ContentType("ivy")]
+  [TagType(typeof(IvyTokenTag))]
+  internal sealed class IvyTokenTagProvider : ITaggerProvider
+  {
+    public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+      return new IvyTokenTagger(buffer) as ITagger<T>;
+    }
+  }
+
+  #endregion
+
+
+  #region Tagger
+
+  public enum IvyTokenKind
+  {
+    Keyword, BuiltInType, Number, String, Comment, VariableIdentifier
+  }
+
+  public class IvyTokenTag : ITag
+  {
+    public IvyTokenKind Kind { get; private set; }
+    public string HoverText
+    {
+      get
+      {
+        string text = "";
+        return text;
+      }
+    }
+
+    public IvyTokenTag(IvyTokenKind kind) {
+      this.Kind = kind;
+    }
+
+  }
+
+
+  internal sealed class IvyTokenTagger : ITagger<IvyTokenTag>, 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 IvyTokenTagger(ITextBuffer buffer) {
+      _buffer = buffer;
+      _snapshot = buffer.CurrentSnapshot;
+      _regions = Scan(_snapshot);
+
+      _buffer.Changed += new EventHandler<TextContentChangedEventArgs>(ReparseFile);
+    }
+
+    public void Dispose() {
+      lock (this) {
+        if (!_disposed) {
+          _buffer.Changed -= ReparseFile;
+          _buffer.Properties.RemoveProperty(bufferTokenTaggerKey);
+          _buffer = null;
+          _snapshot = null;
+          _regions = null;
+          _disposed = true;
+        }
+      }
+      GC.SuppressFinalize(this);
+    }
+
+    public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+    public IEnumerable<ITagSpan<IvyTokenTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+      if (spans.Count == 0)
+        yield break;
+
+      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) {
+        if (entire.IntersectsWith(region.Span)) {
+          yield return new TagSpan<IvyTokenTag>(new SnapshotSpan(region.Start, region.End), new IvyTokenTag(region.Kind));
+        }
+      }
+    }
+
+    /// <summary>
+    /// Find all of the tag regions in the document (snapshot) and notify
+    /// listeners of any that changed
+    /// </summary>
+    void ReparseFile(object sender, TextContentChangedEventArgs args) {
+      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 == IvyTokenKind.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));
+          }
+        }
+
+        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) {
+        foreach (var span in difference) {
+          chng(this, new SnapshotSpanEventArgs(span));
+        }
+      }
+    }
+
+    static NormalizedSnapshotSpanCollection SymmetricDifference(NormalizedSnapshotSpanCollection first, NormalizedSnapshotSpanCollection second) {
+      return NormalizedSnapshotSpanCollection.Union(
+          NormalizedSnapshotSpanCollection.Difference(first, second),
+          NormalizedSnapshotSpanCollection.Difference(second, first));
+    }
+
+    private static SnapshotPoint Scan(string txt, SnapshotPoint start, List<TokenRegion> newRegions, ITextSnapshot newSnapshot) {
+      SnapshotPoint commentStart = new SnapshotPoint();
+      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
+        // 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
+          IvyTokenKind ty = IvyTokenKind.Keyword;
+          for (; ; cur++) {
+            if (N <= cur) {
+              // we've looked at everything in this buffer
+              goto OUTER_CONTINUE;
+            }
+            char ch = txt[cur];
+            if ('a' <= ch && ch <= 'z') break;
+            if ('A' <= ch && ch <= 'Z') break;
+            if ('0' <= ch && ch <= '9') { ty = IvyTokenKind.Number; break; }
+            if (ch == '_' || ch == '?' || ch == '\\') break;  // parts of identifiers
+            if (ch == '\"') { ty = IvyTokenKind.String; break; }
+            if (ch == '#') { ty = IvyTokenKind.Comment; break; }
+          }
+
+          // advance to the end of the token
+          end = cur + 1;  // offset into the current buffer
+
+          if (ty == IvyTokenKind.Number) {
+            // scan the rest of this number
+            for (; end < N; end++) {
+              char ch = txt[end];
+              if ('0' <= ch && ch <= '9' || 'a' <= ch && ch <= 'z' || 'A' <= ch && ch <= 'Z' || ch == '_') {
+              } else break;
+            }
+          } else if (ty == IvyTokenKind.String) {
+            // scan the rest of this string, but not past the end-of-buffer
+            for (; end < N; end++) {
+              char ch = txt[end];
+              if (ch == '\"') {
+                end++; break;
+              } else if (ch == '\\') {
+                // escape sequence
+                end++;
+                if (end == N) { break; }
+                ch = txt[end];
+                if (ch == 'u') {
+                  end += 4;
+                  if (N <= end) { end = N; break; }
+                }
+              }
+            }
+          } else if (ty == IvyTokenKind.Comment) {
+            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];
+	    // a short comment, to the end of the line. (it's all we have)
+            end = newSnapshot.GetLineFromPosition(start + end).End.Position - start;
+          } else {
+            int trailingDigits = 0;
+            for (; end < N; end++) {
+              char ch = txt[end];
+              if ('a' <= ch && ch <= 'z') {
+                trailingDigits = 0;
+              } else if ('A' <= ch && ch <= 'Z') {
+                trailingDigits = 0;
+              } else if ('0' <= ch && ch <= '9') {
+                trailingDigits++;
+              } else if (ch == '_') {
+                trailingDigits = 0;
+              } else break;
+            }
+            // we have a keyword or an identifier
+            string s = txt.Substring(cur, end - cur);
+            {
+              switch (s) {
+                #region keywords
+
+
+		case "relation":
+		case "individual":
+		case "function":
+		case "axiom":
+		case "conjecture":
+		case "schema":
+		case "instantiate":
+		case "instance":
+		case "derived":
+		case "concept":
+		case "init":
+		case "action":
+		case "method":
+		case "state":
+		case "assume":
+		case "assert":
+		case "set":
+		case "null":
+		case "old":
+		case "from":
+		case "update":
+		case "params":
+		case "in":
+		case "match":
+		case "ensures":
+		case "requires":
+		case "modifies":
+		case "true":
+		case "false":
+		case "fresh":
+		case "module":
+		case "object":
+		case "class":
+		case "type":
+		case "if":
+		case "else":
+		case "local":
+		case "let":
+		case "call":
+		case "entry":
+		case "macro":
+		case "interpret":
+		case "forall":
+		case "exists":
+		case "returns":
+		case "mixin":
+		case "execute":
+		case "before":
+		case "after":
+		case "isolate":
+		case "with":
+		case "export":
+		case "delegate":
+		case "import":
+		case "using":
+		case "include":
+		case "progress":
+		case "rely":
+		case "mixord":
+		case "extract":
+		case "destructor":
+		case "some":
+		case "maximizing":
+		case "minimizing":
+		case "private":
+		case "implement":
+		case "property":
+		case "while":
+		case "invariant":
+		case "struct":
+		case "definition":
+		case "ghost":
+		case "alias":
+		case "trusted":
+		case "this":
+		case "var":
+		case "attribute":
+		case "variant":
+		case "of":
+
+                #endregion
+                  break;
+                #region keywords for built-in types
+                case "bool":
+                #endregion
+                  ty = IvyTokenKind.BuiltInType;
+                  break;
+                default:
+                  continue;  // it was an identifier, so we don't color it
+              }
+            }
+          }
+          newRegions.Add(new TokenRegion(new SnapshotPoint(newSnapshot, start + cur), new SnapshotPoint(newSnapshot, start + end), ty));
+        }
+      OUTER_CONTINUE:
+        done = true;
+      }
+      return new SnapshotPoint(newSnapshot, start + N);
+    }
+
+    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;
+    }
+
+    
+  }
+
+  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 IvyTokenKind Kind { get; private set; }
+
+    public TokenRegion(SnapshotPoint start, SnapshotPoint end, IvyTokenKind kind) {
+      Start = start;
+      End = end;
+      Kind = kind;
+    }
+  }
+
+  #endregion
+
+}
--- a/vs/ext/WordHighlighter.cs
+++ b/vs/ext/WordHighlighter.cs
@ -0,0 +1,217 @@
+using System;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using System.Linq;
+using System.Windows.Media;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Classification;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Operations;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+
+
+namespace IvyLanguage
+{
+
+#if LATER_MAYBE
+
+  #region (the current annoying) word highligher
+
+  internal class HighlightWordTagger : ITagger<HighlightWordTag>
+  {
+    ITextView View { get; set; }
+    ITextBuffer SourceBuffer { get; set; }
+    ITextSearchService TextSearchService { get; set; }
+    ITextStructureNavigator TextStructureNavigator { get; set; }
+    NormalizedSnapshotSpanCollection WordSpans { get; set; }
+    SnapshotSpan? CurrentWord { get; set; }
+    SnapshotPoint RequestedPoint { get; set; }
+    object updateLock = new object();
+
+    public HighlightWordTagger(ITextView view, ITextBuffer sourceBuffer, ITextSearchService textSearchService,
+    ITextStructureNavigator textStructureNavigator) {
+      this.View = view;
+      this.SourceBuffer = sourceBuffer;
+      this.TextSearchService = textSearchService;
+      this.TextStructureNavigator = textStructureNavigator;
+      this.WordSpans = new NormalizedSnapshotSpanCollection();
+      this.CurrentWord = null;
+      this.View.Caret.PositionChanged += CaretPositionChanged;
+      this.View.LayoutChanged += ViewLayoutChanged;
+    }
+
+    void ViewLayoutChanged(object sender, TextViewLayoutChangedEventArgs e) {
+      // If a new snapshot wasn't generated, then skip this layout
+      if (e.NewSnapshot != e.OldSnapshot) {
+        UpdateAtCaretPosition(View.Caret.Position);
+      }
+    }
+
+    void CaretPositionChanged(object sender, CaretPositionChangedEventArgs e) {
+      UpdateAtCaretPosition(e.NewPosition);
+    }
+
+    public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+    void UpdateAtCaretPosition(CaretPosition caretPosition) {
+      SnapshotPoint? point = caretPosition.Point.GetPoint(SourceBuffer, caretPosition.Affinity);
+
+      if (!point.HasValue)
+        return;
+
+      // If the new caret position is still within the current word (and on the same snapshot), we don't need to check it
+      if (CurrentWord.HasValue
+          && CurrentWord.Value.Snapshot == View.TextSnapshot
+          && CurrentWord.Value.Start <= point.Value && point.Value <= CurrentWord.Value.End) {
+        return;
+      }
+
+      RequestedPoint = point.Value;
+      UpdateWordAdornments();
+    }
+
+    void UpdateWordAdornments() {
+      SnapshotPoint currentRequest = RequestedPoint;
+      List<SnapshotSpan> wordSpans = new List<SnapshotSpan>();
+      //Find all words in the buffer like the one the caret is on
+      TextExtent word = TextStructureNavigator.GetExtentOfWord(currentRequest);
+      bool foundWord = true;
+      //If we've selected something not worth highlighting, we might have missed a "word" by a little bit
+      if (!WordExtentIsValid(currentRequest, word)) {
+        //Before we retry, make sure it is worthwhile
+        if (word.Span.Start != currentRequest
+             || currentRequest == currentRequest.GetContainingLine().Start
+             || char.IsWhiteSpace((currentRequest - 1).GetChar())) {
+          foundWord = false;
+        } else {
+          // Try again, one character previous.
+          //If the caret is at the end of a word, pick up the word.
+          word = TextStructureNavigator.GetExtentOfWord(currentRequest - 1);
+
+          //If the word still isn't valid, we're done
+          if (!WordExtentIsValid(currentRequest, word))
+            foundWord = false;
+        }
+      }
+
+      if (!foundWord) {
+        //If we couldn't find a word, clear out the existing markers
+        SynchronousUpdate(currentRequest, new NormalizedSnapshotSpanCollection(), null);
+        return;
+      }
+
+      SnapshotSpan currentWord = word.Span;
+      //If this is the current word, and the caret moved within a word, we're done.
+      if (CurrentWord.HasValue && currentWord == CurrentWord)
+        return;
+
+      //Find the new spans
+      FindData findData = new FindData(currentWord.GetText(), currentWord.Snapshot);
+      findData.FindOptions = FindOptions.WholeWord | FindOptions.MatchCase;
+
+      wordSpans.AddRange(TextSearchService.FindAll(findData));
+
+      //If another change hasn't happened, do a real update
+      if (currentRequest == RequestedPoint)
+        SynchronousUpdate(currentRequest, new NormalizedSnapshotSpanCollection(wordSpans), currentWord);
+    }
+
+    static bool WordExtentIsValid(SnapshotPoint currentRequest, TextExtent word) {
+      return word.IsSignificant
+          && currentRequest.Snapshot.GetText(word.Span).Any(c => char.IsLetter(c));
+    }
+
+    void SynchronousUpdate(SnapshotPoint currentRequest, NormalizedSnapshotSpanCollection newSpans, SnapshotSpan? newCurrentWord) {
+      lock (updateLock) {
+        if (currentRequest != RequestedPoint)
+          return;
+
+        WordSpans = newSpans;
+        CurrentWord = newCurrentWord;
+
+        var chngd = TagsChanged;
+        if (chngd != null)
+          chngd(this, new SnapshotSpanEventArgs(new SnapshotSpan(SourceBuffer.CurrentSnapshot, 0, SourceBuffer.CurrentSnapshot.Length)));
+      }
+    }
+
+    public IEnumerable<ITagSpan<HighlightWordTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+      if (CurrentWord == null)
+        yield break;
+
+      // Hold on to a "snapshot" of the word spans and current word, so that we maintain the same
+      // collection throughout
+      SnapshotSpan currentWord = CurrentWord.Value;
+      NormalizedSnapshotSpanCollection wordSpans = WordSpans;
+
+      if (spans.Count == 0 || WordSpans.Count == 0)
+        yield break;
+
+      // If the requested snapshot isn't the same as the one our words are on, translate our spans to the expected snapshot
+      if (spans[0].Snapshot != wordSpans[0].Snapshot) {
+        wordSpans = new NormalizedSnapshotSpanCollection(
+            wordSpans.Select(span => span.TranslateTo(spans[0].Snapshot, SpanTrackingMode.EdgeExclusive)));
+
+        currentWord = currentWord.TranslateTo(spans[0].Snapshot, SpanTrackingMode.EdgeExclusive);
+      }
+
+      // First, yield back the word the cursor is under (if it overlaps)
+      // Note that we'll yield back the same word again in the wordspans collection;
+      // the duplication here is expected.
+      if (spans.OverlapsWith(new NormalizedSnapshotSpanCollection(currentWord)))
+        yield return new TagSpan<HighlightWordTag>(currentWord, new HighlightWordTag());
+
+      // Second, yield all the other words in the file
+      foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, wordSpans)) {
+        yield return new TagSpan<HighlightWordTag>(span, new HighlightWordTag());
+      }
+    }
+  }
+
+  internal class HighlightWordTag : TextMarkerTag
+  {
+    public HighlightWordTag() : base("MarkerFormatDefinition/HighlightWordFormatDefinition") { }
+  }
+
+  [Export(typeof(EditorFormatDefinition))]
+  [Name("MarkerFormatDefinition/HighlightWordFormatDefinition")]
+  [UserVisible(true)]
+  internal class HighlightWordFormatDefinition : MarkerFormatDefinition
+  {
+    public HighlightWordFormatDefinition() {
+      this.BackgroundColor = Colors.LightBlue;
+      this.ForegroundColor = Colors.DarkBlue;
+      this.DisplayName = "Highlight Word";
+      this.ZOrder = 5;
+    }
+  }
+
+  [Export(typeof(IViewTaggerProvider))]
+  [ContentType("text")]
+  [TagType(typeof(TextMarkerTag))]
+  internal class HighlightWordTaggerProvider : IViewTaggerProvider
+  {
+    [Import]
+    internal ITextSearchService TextSearchService { get; set; }
+
+    [Import]
+    internal ITextStructureNavigatorSelectorService TextStructureNavigatorSelector { get; set; }
+
+    public ITagger<T> CreateTagger<T>(ITextView textView, ITextBuffer buffer) where T : ITag {
+      //provide highlighting only on the top buffer
+      if (textView.TextBuffer != buffer)
+        return null;
+
+      ITextStructureNavigator textStructureNavigator =
+          TextStructureNavigatorSelector.GetTextStructureNavigator(buffer);
+
+      return new HighlightWordTagger(textView, buffer, TextSearchService, textStructureNavigator) as ITagger<T>;
+    }
+  }
+
+  #endregion
+
+#endif
+
+}
--- a/vs/ext/packages.config
+++ b/vs/ext/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>
--- a/vs/ext/source.extension.vsixmanifest
+++ b/vs/ext/source.extension.vsixmanifest
@ -0,0 +1,21 @@
+<?xml version="1.0" encoding="utf-8"?>
+<PackageManifest Version="2.0.0" xmlns="http://schemas.microsoft.com/developer/vsx-schema/2011" xmlns:d="http://schemas.microsoft.com/developer/vsx-schema-design/2011">
+  <Metadata>
+    <Identity Id="6c7ed99a-206a-4937-9e08-b389de175f68" Version="1.9.3.20406" Language="en-US" Publisher="Microsoft Research" />
+    <DisplayName>IvyLanguageMode</DisplayName>
+    <Description xml:space="preserve">This is a language mode for using the Ivy language inside Visual Studio.</Description>
+    <License>Z3-LICENSE.txt</License>
+  </Metadata>
+  <Installation InstalledByMsi="false">
+    <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.VisualStudio.MPF.11.0" DisplayName="Visual Studio MPF 11.0" d:Source="Installed" Version="11.0" />
+  </Dependencies>
+  <Assets>
+    <Asset Type="Microsoft.VisualStudio.VsPackage" d:Source="Project" d:ProjectName="%CurrentProject%" Path="|%CurrentProject%;PkgdefProjectOutputGroup|" />
+    <Asset Type="Microsoft.VisualStudio.MefComponent" d:Source="Project" d:ProjectName="%CurrentProject%" Path="|%CurrentProject%|" />
+  </Assets>
+</PackageManifest>