Add tooltip on assertions that shows which functions are hidden

Source/DafnyCore/AST/Tokens.cs

@@ -204,6 +204,15 @@ public int CompareTo(IToken other) {
   public int CompareTo(Boogie.IToken other) {
     return WrappedToken.CompareTo(other);
   }
+
+  public static IToken Unwrap(IToken token, bool includeRanges = false) {
+    if (token is TokenWrapper wrapper
+        && (includeRanges || token is not RangeToken)) {
+      return Unwrap(wrapper.WrappedToken);
+    }
+
+    return token;
+  }
 }
 
 public static class TokenExtensions {

Source/DafnyCore/Pipeline/Compilation.cs

@@ -363,12 +363,14 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT
       await ticket;
 
       if (!onlyPrepareVerificationForGutterTests) {
-        foreach (var tokenTasks in tasks.GroupBy(t =>
-                  BoogieGenerator.ToDafnyToken(true, t.Token)).
-                  OrderBy(g => g.Key)) {
+        var groups = tasks.GroupBy(t =>
+            // We unwrap so that we group on tokens as they are displayed to the user by Reporter.Info
+            TokenWrapper.Unwrap(BoogieGenerator.ToDafnyToken(true, t.Token))).
+          OrderBy(g => g.Key);
+        foreach (var tokenTasks in groups) {
           var functions = tokenTasks.SelectMany(t => t.Split.HiddenFunctions.Select(f => f.tok).
             OfType<FromDafnyNode>().Select(n => n.Node).
-            OfType<Function>()).Distinct();
+            OfType<Function>()).Distinct().OrderBy(f => f.tok);
           var hiddenFunctions = string.Join(", ", functions.Select(f => f.FullDafnyName));
           if (!string.IsNullOrEmpty(hiddenFunctions)) {
             Reporter.Info(MessageSource.Verifier, tokenTasks.Key, $"hidden functions: {hiddenFunctions}");

Source/DafnyLanguageServer.Test/Diagnostics/DiagnosticsTest.cs

@@ -1331,11 +1331,105 @@ assert Outer(3) by {
     reveal Outer, Inner;
   }
 }
+
+
 ".TrimStart();
       var documentItem = CreateTestDocument(source, "HiddenFunctionHints.dfy");
       client.OpenDocument(documentItem);
       var diagnostics = await GetLastDiagnostics(documentItem, minimumSeverity: DiagnosticSeverity.Hint);
+
       Assert.Equal(6, diagnostics.Length);
+      var sorted = diagnostics.OrderBy(d => d.Range.Start).ToList();
+      for (int index = 0; index < 3; index++) {
+        Assert.Equal(sorted[index * 2].Range, sorted[index * 2 + 1].Range);
+      }
+    }
+
+    [Fact]
+    public async Task HiddenFunctionTooltipBlowup() {
+      var source = @"
+predicate A(x: int) {
+  x < 5
+}
+predicate B(x: int) {
+  x > 3
+}
+predicate P(x: int) {
+  A(x) && B(x)
+}
+
+method {:isolate_assertions} TestIsolateAssertions() {
+  hide *;
+  assert P(3);
+}
+".TrimStart();
+      var documentItem = CreateTestDocument(source, "HiddenFunctionHints.dfy");
+      client.OpenDocument(documentItem);
+      var diagnostics = await GetLastDiagnostics(documentItem, minimumSeverity: DiagnosticSeverity.Hint);
+
+      var infoDiagnostics = diagnostics.Where(d => d.Severity >= DiagnosticSeverity.Information).ToList();
+      Assert.Single(infoDiagnostics);
+    }
+
+    [Fact]
+    public async Task HiddenFunctionTooltipBlowup2() {
+      var source = @"
+predicate A(x: int) {
+  x < 5
+}
+predicate B(x: int) {
+  x > 3
+}
+predicate P(x: int) {
+  A(x) && B(x)
+}
+
+method {:isolate_assertions} TestIsolateAssertions() {
+  hide *;
+  reveal P;
+  assert P(3);
+}
+".TrimStart();
+      var documentItem = CreateTestDocument(source, "HiddenFunctionHints.dfy");
+      client.OpenDocument(documentItem);
+      var diagnostics = await GetLastDiagnostics(documentItem, minimumSeverity: DiagnosticSeverity.Hint);
+
+      var infoDiagnostics = diagnostics.Where(d => d.Severity >= DiagnosticSeverity.Information).ToList();
+      Assert.Single(infoDiagnostics);
+    }
+
+    [Fact]
+    public async Task HiddenFunctionTooltipBlowup3() {
+      var source = @"
+predicate A(x: int) {
+  x < 7 && C(x)
+}
+predicate B(x: int) {
+  x > 3
+}
+
+predicate C(x: int) {
+  x < 5
+}
+
+predicate P(x: int)
+  requires A(x) && B(x)
+{
+  true
+}
+
+method {:isolate_assertions} TestIsolateAssertions() {
+  hide *;
+  reveal P;
+  assert P(6);
+}
+".TrimStart();
+      var documentItem = CreateTestDocument(source, "HiddenFunctionHints.dfy");
+      client.OpenDocument(documentItem);
+      var diagnostics = await GetLastDiagnostics(documentItem, minimumSeverity: DiagnosticSeverity.Hint);
+
+      var infoDiagnostics = diagnostics.Where(d => d.Severity >= DiagnosticSeverity.Information).ToList();
+      Assert.Single(infoDiagnostics);
     }
 
     public DiagnosticsTest(ITestOutputHelper output) : base(output) {