From fc821745ae24ae9d43725aaecfcece6735cc232e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 23 Jun 2021 23:29:46 +0200 Subject: [PATCH] fix: swallow exception on hover formatting --- src/Lean/Server/InfoUtils.lean | 6 ++++-- tests/lean/interactive/hoverException.lean | 3 +++ tests/lean/interactive/hoverException.lean.expected.out | 3 +++ 3 files changed, 10 insertions(+), 2 deletions(-) create mode 100644 tests/lean/interactive/hoverException.lean create mode 100644 tests/lean/interactive/hoverException.lean.expected.out diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 136e9f6167..26d9770a60 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -131,8 +131,10 @@ partial def InfoTree.hoverableInfoAt? (t : InfoTree) (hoverPos : String.Pos) : O def Info.fmtHover? (ci : ContextInfo) (i : Info) : IO (Option Format) := do ci.runMetaM i.lctx do let mut fmts := #[] - if let some f ← fmtTerm? then - fmts := fmts.push f + try + if let some f ← fmtTerm? then + fmts := fmts.push f + catch _ => pure () if let some f ← fmtDoc? then fmts := fmts.push f if fmts.isEmpty then diff --git a/tests/lean/interactive/hoverException.lean b/tests/lean/interactive/hoverException.lean new file mode 100644 index 0000000000..6e56570b65 --- /dev/null +++ b/tests/lean/interactive/hoverException.lean @@ -0,0 +1,3 @@ +inductive Foo +| mk : (a b : Bar) → Foo + --^ textDocument/hover diff --git a/tests/lean/interactive/hoverException.lean.expected.out b/tests/lean/interactive/hoverException.lean.expected.out new file mode 100644 index 0000000000..311e2c9b53 --- /dev/null +++ b/tests/lean/interactive/hoverException.lean.expected.out @@ -0,0 +1,3 @@ +{"textDocument": {"uri": "file://hoverException.lean"}, + "position": {"line": 1, "character": 14}} +null