DafnyExtension: Added support for collecting additional information during resolution and displaying it.

1 files changed, 25 insertions, 1 deletions

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 49c7bb01..e334271f 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -87,6 +87,8 @@ namespace DafnyLanguage
               kind = DafnyTokenKind.VariableIdentifierDefinition; break;

             case IdRegion.OccurrenceKind.WildDefinition:

               kind = DafnyTokenKind.Keyword; break;

+            case IdRegion.OccurrenceKind.AdditionalInformation:

+              kind = DafnyTokenKind.AdditionalInformation; break;

             default:

               Contract.Assert(false);  // unexpected OccurrenceKind

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

@@ -134,6 +136,11 @@ namespace DafnyLanguage
 

       List<IdRegion> newRegions = new List<IdRegion>();

 

+      foreach (var addInfo in program.AdditionalInformation)

+      {

+        IdRegion.Add(newRegions, addInfo.Token, addInfo.Text, addInfo.Length);

+      }

+

       foreach (var module in program.Modules) {

         if (module.IsFacade) {

           continue;

@@ -316,7 +323,7 @@ namespace DafnyLanguage
       public readonly int Start;

       public readonly int Length;

       public readonly string HoverText;

-      public enum OccurrenceKind { Use, Definition, WildDefinition }

+      public enum OccurrenceKind { Use, Definition, WildDefinition, AdditionalInformation }

       public readonly OccurrenceKind Kind;

 

       static bool SurfaceSyntaxToken(Bpl.IToken tok) {

@@ -348,6 +355,15 @@ namespace DafnyLanguage
         }

       }

 

+      public static void Add(List<IdRegion> regions, Bpl.IToken tok, string text, int length) {

+        Contract.Requires(regions != null);

+        Contract.Requires(tok != null);

+        Contract.Requires(text != null);

+        if (SurfaceSyntaxToken(tok)) {

+          regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length));

+        }

+      }

+

       private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) {

         Contract.Requires(tok != null);

         Contract.Requires(v != null);

@@ -385,6 +401,14 @@ namespace DafnyLanguage
           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;

+      }

     }

   }