From 56b967ee7ad15526a27f6d3fab63e6f9712984d4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 22 May 2023 16:00:41 -0700 Subject: [PATCH] Add module name for symbol --- Main.lean | 10 ++++++++-- Pantograph/Commands.lean | 3 ++- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/Main.lean b/Main.lean index fcb2190..f3ec8dc 100644 --- a/Main.lean +++ b/Main.lean @@ -125,7 +125,8 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do match state.getEnv args.id with | .error error => return Lean.toJson <| errorIndex error | .ok env => - let info? := env.find? <| str_to_name args.symbol + let name := str_to_name args.symbol + let info? := env.find? name match info? with | none => return Lean.toJson <| errorIndex s!"Symbol not found {args.symbol}" | some info => @@ -133,7 +134,12 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do (env := env) (coreContext := context.coreContext) (expr := info.toConstantVal.type) - return Lean.toJson ({ type := format }: InspectResult) + let module? := env.getModuleIdxFor? name >>= + (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString + return Lean.toJson ({ + type := format, + module? := module? + }: InspectResult) proof_start (args: ProofStart): Subroutine Lean.Json := do let context ← read let state ← get diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index d90715a..353d162 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -45,7 +45,8 @@ structure Inspect where symbol: String deriving Lean.FromJson structure InspectResult where - type: String := "" + type: String + module?: Option String deriving Lean.ToJson structure ProofStart where