Fixed up VS plug-in to handle shared destructors

Rustan Leino · Rustan Leino · commit 68a0f31d06af · 2017-04-16T12:24:45.000-07:00
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
@@ -152,8 +152,10 @@ bool ComputeIdentifierRegions(Microsoft.Dafny.Program program, ITextSnapshot sna
             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);
+                var i = dtor.EnclosingCtors.IndexOf(ctor);
+                var formal = dtor.CorrespondingFormals[i];
+                if (formal.HasName) {
+                  IdRegion.Add(newRegions, program, formal.tok, dtor, null, "destructor", true, module);
                 }
               }
             }

Original file line number	Diff line number	Diff line change
`@@ -152,8 +152,10 @@ bool ComputeIdentifierRegions(Microsoft.Dafny.Program program, ITextSnapshot sna`
`152`	`152`	`var dt = (DatatypeDecl)d;`
`153`	`153`	`foreach (var ctor in dt.Ctors) {`
`154`	`154`	`foreach (var dtor in ctor.Destructors) {`
`155`		`- if (dtor.CorrespondingFormal.HasName) {`
`156`		`- IdRegion.Add(newRegions, program, dtor.tok, dtor, null, "destructor", true, module);`
	`155`	`+ var i = dtor.EnclosingCtors.IndexOf(ctor);`
	`156`	`+ var formal = dtor.CorrespondingFormals[i];`
	`157`	`+ if (formal.HasName) {`
	`158`	`+ IdRegion.Add(newRegions, program, formal.tok, dtor, null, "destructor", true, module);`
`157`	`159`	`}`
`158`	`160`	`}`
`159`	`161`	`}`