aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 16 Pull Requests 3 Packages Projects Releases Wiki Activity

fix(env): Use documentUriFromModule

This commit is contained in:
Leni Aniva 2025-06-17 11:10:52 -07:00
parent b2b7cc388a
commit a8b7f69632
Signed by: aniva
GPG Key ID: D5F96287843E8DFB
1 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Pantograph/Environment.lean
View File

@ -131,9 +131,8 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
} } } }
| _ => pure core | _ => pure core
let result ← if args.source?.getD false then let result ← if args.source?.getD false then
let srcSearchPath ← getSrcSearchPath
try try
let sourceUri? ← module?.mapM (findLean srcSearchPath ·) let sourceUri? ← module?.bindM (Server.documentUriFromModule? ·)
let declRange? ← findDeclarationRanges? name let declRange? ← findDeclarationRanges? name
let sourceStart? := declRange?.map (·.range.pos) let sourceStart? := declRange?.map (·.range.pos)
let sourceEnd? := declRange?.map (·.range.endPos) let sourceEnd? := declRange?.map (·.range.endPos)
@ -143,7 +142,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
sourceStart?, sourceStart?,
sourceEnd?, sourceEnd?,
} }
catch _ => catch _e =>
.pure result .pure result
else else
.pure result .pure result