From 9bfbabb9dfaee47d4994ae26463900fab9c80a24 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 30 Aug 2022 18:07:18 +0200
Subject: [PATCH] fix: do not fail widget request after `#exit`

---
 src/Lean/Widget/UserWidget.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean
index c4f454e805..147d0fa7d8 100644
--- a/src/Lean/Widget/UserWidget.lean
+++ b/src/Lean/Widget/UserWidget.lean
@@ -145,7 +145,7 @@ def getWidgets (args : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsRes
   let doc ← readDoc
   let filemap := doc.meta.text
   let pos := filemap.lspPosToUtf8Pos args
-  withWaitFindSnapAtPos args fun snap => do
+  withWaitFindSnap doc (·.endPos >= pos) (notFoundX := return ⟨∅⟩) fun snap => do
     let env := snap.env
     let ws := widgetInfosAt? filemap snap.infoTree pos
     let ws ← ws.toArray.mapM (fun (w : UserWidgetInfo) => do