From a8b7f69632592456d0c123989ac4c285fb8a60e0 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 17 Jun 2025 11:10:52 -0700 Subject: [PATCH] fix(env): Use documentUriFromModule --- Pantograph/Environment.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index dce74c8..f52e7d2 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -131,9 +131,8 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol. } } | _ => pure core let result ← if args.source?.getD false then - let srcSearchPath ← getSrcSearchPath try - let sourceUri? ← module?.mapM (findLean srcSearchPath ·) + let sourceUri? ← module?.bindM (Server.documentUriFromModule? ·) let declRange? ← findDeclarationRanges? name let sourceStart? := declRange?.map (·.range.pos) let sourceEnd? := declRange?.map (·.range.endPos) @@ -143,7 +142,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol. sourceStart?, sourceEnd?, } - catch _ => + catch _e => .pure result else .pure result