From 3ca52e0f1bdc1ee0edfe19f774661bf02bf0e6b3 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Mon, 29 Jun 2015 15:18:31 -0700
Subject: Fix identifiers in nested match patterns not showing in the IDE bug.
 Remember BoundVars that are combined in rewriting of the nested match
 patterns so they show up in the IDE correctly.

---
 Source/DafnyExtension/IdentifierTagger.cs | 24 ++++++++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

(limited to 'Source/DafnyExtension')

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 086ac8e4..262dddcd 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -270,7 +270,17 @@ namespace DafnyLanguage
       } else if (expr is MatchExpr) {
         var e = (MatchExpr)expr;
         foreach (var kase in e.Cases) {
-          kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
+          kase.Arguments.ForEach(bv => {
+            IdRegion.Add(regions, bv.tok, bv, true, 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, entry.Item1, entry.Item2, entry.Item3, module);
+              }
+            }
+          });
         }
       } else if (expr is ChainingExpression) {
         var e = (ChainingExpression)expr;
@@ -313,7 +323,17 @@ namespace DafnyLanguage
       } else if (stmt is MatchStmt) {
         var s = (MatchStmt)stmt;
         foreach (var kase in s.Cases) {
-          kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
+          kase.Arguments.ForEach(bv => {
+            IdRegion.Add(regions, bv.tok, bv, true, 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, entry.Item1, entry.Item2, entry.Item3, module);
+              }
+            }              
+          });
         }
       } else if (stmt is LoopStmt) {
         var s = (LoopStmt)stmt;
-- 
cgit v1.2.3