Pantograph/Environment.lean

@@ -58,7 +58,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
     | none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
     | some info => pure info
   let module? := env.getModuleIdxFor? name >>=
-    (λ idx => env.allImportedModuleNames.get? idx.toNat)
+    (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
   let value? := match args.value?, info with
     | .some true, _ => info.value?
     | .some false, _ => .none
@@ -80,7 +80,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
       then value?.map (λ e =>
         e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
       else .none,
-    module? := module?.map (·.toString)
+    module? := module?
   }
   let result ← match info with
     | .inductInfo induct => pure { core with inductInfo? := .some {
@@ -113,20 +113,6 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
           k := r.k,
       } }
     | _ => pure core
-  let result ← if args.source?.getD false then
-      let srcSearchPath ← initSrcSearchPath
-      let sourceUri? ← module?.bindM (Server.documentUriFromModule srcSearchPath ·)
-      let declRange? ← findDeclarationRanges? name
-      let sourceStart? := declRange?.map (·.range.pos)
-      let sourceEnd? := declRange?.map (·.range.endPos)
-      .pure {
-        result with
-        sourceUri?,
-        sourceStart?,
-        sourceEnd?,
-      }
-    else
-      .pure result
   return .ok result
 def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
   let env ← Lean.MonadEnv.getEnv

Pantograph/Protocol.lean

@@ -5,7 +5,6 @@ Note that no command other than `InteractionError` may have `error` as one of
 its field names to avoid confusion with error messages generated by the REPL.
 -/
 import Lean.Data.Json
-import Lean.Data.Position
 
 namespace Pantograph.Protocol
 
@@ -122,13 +121,11 @@ structure EnvCatalogResult where
 -- Print the type of a symbol
 structure EnvInspect where
   name: String
-  -- Show the value expressions; By default definitions values are shown and
+  -- If true/false, show/hide the value expressions; By default definitions
-  -- theorem values are hidden.
+  -- values are shown and theorem values are hidden.
   value?: Option Bool := .some false
-  -- Show the type and value dependencies
+  -- If true, show the type and value dependencies
   dependency?: Option Bool := .some false
-  -- Show source location
-  source?: Option Bool := .some false
   deriving Lean.FromJson
 -- See `InductiveVal`
 structure InductInfo where
@@ -175,11 +172,6 @@ structure EnvInspectResult where
   inductInfo?:      Option InductInfo      := .none
   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
   deriving Lean.ToJson
 
 structure EnvAdd where

Test/Common.lean

@@ -143,8 +143,6 @@ 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,26 +97,11 @@ 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