From 8d1676a6d30e295d57e7e64fc58d103771459974 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Mon, 27 Jul 2015 11:28:39 -0700
Subject: Clarify the inlining warning.

---
 Source/Dafny/Translator.cs | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'Source')

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e2c45558..83078fb5 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -12956,12 +12956,8 @@ namespace Microsoft.Dafny {
           } else {
             // Skip inlining, as it would cause arbitrary expressions to pop up in the trigger
             // CLEMENT: Report inlining issue in a VS plugin friendly way
-            var info = new AdditionalInformation {
-              Token = fexp.tok,
-              Length = fexp.tok.val.Length,
-              Text = "This call cannot be safely inlined.",
-            };
-            Resolver.DefaultInformationReporter(info);
+            //CLEMENT this should appear at the outmost call site, not at the innermost. See SnapshotableTrees.dfy
+            Dafny.Util.ReportIssue("Info", fexp.tok, "Some instances of this call cannot safely be inlined.");
           }
         }
 
-- 
cgit v1.2.3