Added {:auto_generated} trigger, which indicates that a declaration was not explicitly mentioned in the input. This lets the Dafny IDE know not to add hovertext for these declarations.

1 files changed, 3 insertions, 1 deletions

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 3bb8f01c..086ac8e4 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -179,7 +179,9 @@ namespace DafnyLanguage
           } else if (d is ClassDecl) {

             var cl = (ClassDecl)d;

             foreach (var member in cl.Members) {

-              if (member is Function) {

+              if (Attributes.Contains(member.Attributes, "auto_generated")) {

+                // do nothing

+              } else  if (member is Function) {

                 var f = (Function)member;

                 foreach (var p in f.Formals) {

                   IdRegion.Add(newRegions, p.tok, p, true, module);