From 377d6e8bcc3677e2242be51fbd2d31e836976fa8 Mon Sep 17 00:00:00 2001
From: Julian Berman <Julian@GrayVines.com>
Date: Wed, 2 Oct 2024 12:23:58 -0400
Subject: [PATCH] Add a failing?? test for multiple widget suggestion contents.

This works interactively so it must be failing for some trivial
reason again.

Needs some diagnosing but leaving it here just to remind myself
to add this test when we get it working.
---
 spec/infoview/widgets_spec.lua | 42 ++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/spec/infoview/widgets_spec.lua b/spec/infoview/widgets_spec.lua
index c7c4d016..e863a2ee 100644
--- a/spec/infoview/widgets_spec.lua
+++ b/spec/infoview/widgets_spec.lua
@@ -65,4 +65,46 @@ describe('widgets', function()
       end
     )
   )
+
+  it(
+    'supports try this widgets with multiple suggestions',
+    helpers.clean_buffer(
+      [[
+        import Lean.Meta.Tactic.TryThis
+
+        namespace Lean.Meta.Tactic.TryThis
+        open Lean Elab Tactic
+
+        elab "twoSuggestions" : tactic => do
+          addSuggestion (← getRef) (← `(tactic| trivial))
+          addSuggestion (← getRef) (← `(tactic| rfl))
+
+        example : 37 = 37 := by twoSuggestions
+
+        end Lean.Meta.Tactic.TryThis
+      ]],
+      function()
+        helpers.move_cursor { to = { 10, 28 } }
+        assert.infoview_contents.are [[
+          ⊢ 37 = 37
+
+          ▶ 10:25-10:39: information:
+          Try this: trivial
+
+          ▶ 10:25-10:39: information:
+          Try this: rfl
+
+          ▶ 10:22-10:39: error:
+          unsolved goals
+          ⊢ 37 = 37
+
+          ▶ suggestions:
+          trivial
+
+          ▶ suggestions:
+          rfl
+        ]]
+      end
+    )
+  )
 end)