From 484e5102216badf51e3738242c45c982895f8d6c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 2 Jun 2022 16:22:43 -0700 Subject: [PATCH] feat: do not use `pp.inaccessibleNames = true` at `getInteractiveTermGoal` See discussion at https://github.com/leanprover/vscode-lean4/issues/76 We also use `pp.inaccessibleNames = false` in error messages. In this setting, an inaccessible name is displayed in the context only if the target type depends on it. --- src/Lean/Server/FileWorker/RequestHandling.lean | 2 +- tests/lean/interactive/expectedTypeAsGoal.lean | 9 +++++++++ .../interactive/expectedTypeAsGoal.lean.expected.out | 5 +++++ 3 files changed, 15 insertions(+), 1 deletion(-) create mode 100644 tests/lean/interactive/expectedTypeAsGoal.lean create mode 100644 tests/lean/interactive/expectedTypeAsGoal.lean.expected.out diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index fdc4a57f45..23ece3a5b0 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -183,7 +183,7 @@ def getInteractiveTermGoal (p : Lsp.PlainTermGoalParams) -- for binders, hide the last hypothesis (the binder itself) let lctx' := if ti.isBinder then i.lctx.pop else i.lctx let goal ← ci.runMetaM lctx' do - Meta.withPPInaccessibleNames <| Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId! + Widget.goalToInteractive (← Meta.mkFreshExprMVar ty).mvarId! let range := if let some r := i.range? then r.toLspRange text else ⟨p.position, p.position⟩ return some { goal with range } else diff --git a/tests/lean/interactive/expectedTypeAsGoal.lean b/tests/lean/interactive/expectedTypeAsGoal.lean new file mode 100644 index 0000000000..78f2237537 --- /dev/null +++ b/tests/lean/interactive/expectedTypeAsGoal.lean @@ -0,0 +1,9 @@ +def big : IO Unit := do + let x := 10 + if true then + IO.println s!"a{x}" + --^ $/lean/plainTermGoal + if false then + IO.println "b" + if 1 < 3 then + IO.println "c" diff --git a/tests/lean/interactive/expectedTypeAsGoal.lean.expected.out b/tests/lean/interactive/expectedTypeAsGoal.lean.expected.out new file mode 100644 index 0000000000..1c6ad9bbf7 --- /dev/null +++ b/tests/lean/interactive/expectedTypeAsGoal.lean.expected.out @@ -0,0 +1,5 @@ +{"textDocument": {"uri": "file://expectedTypeAsGoal.lean"}, + "position": {"line": 3, "character": 5}} +{"range": + {"start": {"line": 3, "character": 4}, "end": {"line": 3, "character": 23}}, + "goal": "x : Nat := 10\n⊢ IO Unit"}