Pantograph/Environment.lean

@@ -114,8 +114,8 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
       } }
     | _ => pure core
   let result ← if args.source?.getD false then
-      let searchPath ← searchPathRef.get
+      let srcSearchPath ← initSrcSearchPath
-      let sourceUri? ← module?.bindM (Server.documentUriFromModule searchPath ·)
+      let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·)
       let declRange? ← findDeclarationRanges? name
       let sourceStart? := declRange?.map (·.range.pos)
       let sourceEnd? := declRange?.map (·.range.endPos)

Pantograph/Protocol.lean

@@ -176,6 +176,7 @@ structure EnvInspectResult where
   constructorInfo?: Option ConstructorInfo := .none
   recursorInfo?:    Option RecursorInfo    := .none
 
+  -- Location in source
   sourceUri?: Option String := .none
   sourceStart?: Option Lean.Position := .none
   sourceEnd?: Option Lean.Position := .none

Test/Common.lean

@@ -143,6 +143,8 @@ def runTest (t: TestT m Unit): m LSpec.TestSeq :=
   Prod.snd <$> t.run LSpec.TestSeq.done
 def runTestWithResult { α } (t: TestT m α): m (α × LSpec.TestSeq) :=
   t.run LSpec.TestSeq.done
+def runTestCoreM (env: Environment) (coreM: TestT CoreM Unit) (options: Array String := #[]): IO LSpec.TestSeq := do
+  runCoreMSeq env (runTest coreM) options
 
 end Monadic
 

Test/Environment.lean

@@ -97,11 +97,26 @@ def test_inspect: IO LSpec.TestSeq := do
     ) LSpec.TestSeq.done
   runCoreMSeq env inner
 
+def test_symbol_location : TestT IO Unit := do
+  let env: Environment ← importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
+  addTest $ ← runTestCoreM env do
+    let .ok result ← Environment.inspect { name := "Nat.le_of_succ_le", source? := .some true } (options := {}) | fail "Inspect failed"
+    checkEq "module" result.module? <| .some "Init.Data.Nat.Basic"
+
+    -- Doesn't work for symbols in `Init` for some reason
+    --checkEq "file" result.sourceUri? <| .some "??"
+    checkEq "pos" result.sourceStart? <| .some { line := 344, column := 0 }
+    checkEq "pos" result.sourceEnd? <| .some { line := 344, column := 88 }
+
 def suite: List (String × IO LSpec.TestSeq) :=
   [
     ("Catalog", test_catalog),
     ("Symbol Visibility", test_symbol_visibility),
     ("Inspect", test_inspect),
+    ("Symbol Location", runTest test_symbol_location),
   ]
 
 end Pantograph.Test.Environment