max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: prefer syntax doc over elab when both are present

Browse source 
closes #1443
This commit is contained in:
Mario Carneiro 2022-08-12 08:45:49 -04:00 • committed by Leonardo de Moura
parent 311d376bde
commit 1302d8f7fc
2 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Server/InfoUtils.lean
View file

@ -192,7 +192,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
if let Info.ofFieldInfo fi := i then
return ← findDocString? env fi.projName
if let some ei := i.toElabInfo? then
return ← findDocString? env ei.elaborator <||> findDocString? env ei.stx.getKind
return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator
return none
/-- Construct a hover popup, if any, from an info node in a context.-/

9
tests/lean/interactive/hover.lean.expected.out
View file

@ -76,12 +76,12 @@
"position": {"line": 36, "character": 2}}
{"range":
{"start": {"line": 36, "character": 2}, "end": {"line": 36, "character": 23}},
"contents": {"value": "My way better tactic ", "kind": "markdown"}}
"contents": {"value": "My tactic ", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 44, "character": 2}}
{"range":
{"start": {"line": 44, "character": 2}, "end": {"line": 44, "character": 23}},
"contents": {"value": "My way better tactic ", "kind": "markdown"}}
"contents": {"value": "My tactic ", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 51, "character": 7}}
{"range":
@ -93,8 +93,7 @@
{"range":
{"start": {"line": 58, "character": 7}, "end": {"line": 58, "character": 15}},
"contents":
{"value": "```lean\nNat\n```\n***\nMy way better notation ",
"kind": "markdown"}}
{"value": "```lean\nNat\n```\n***\nMy notation ", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 68, "character": 7}}
{"range":
@ -124,7 +123,7 @@
"position": {"line": 86, "character": 2}}
{"range":
{"start": {"line": 86, "character": 0}, "end": {"line": 86, "character": 7}},
"contents": {"value": "My way better command ", "kind": "markdown"}}
"contents": {"value": "My command ", "kind": "markdown"}}
{"textDocument": {"uri": "file://hover.lean"},
"position": {"line": 89, "character": 16}}
{"range":