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

chore: add location

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-04 10:50:30 -07:00
parent 820495ce7a
commit cffef2674f
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/InfoTree.lean
View file

@ -161,8 +161,8 @@ def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
match info with
| CompletionInfo.dot i .. => return f!"[.] {← i.format ctx}"
| CompletionInfo.id stx lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {stx} : {expectedType?}"
| _ => return f!"[.] {info.stx}"
| CompletionInfo.id stx lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
| _ => return f!"[.] {info.stx} @ {formatStxRange ctx info.stx}"
def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := do
return f!"command @ {formatStxRange ctx info.stx}"