From 4f5ffc1ffbc00a0b21fe0f12514a75fc925701b3 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 15 Jan 2025 21:02:04 -0800 Subject: [PATCH] feat: Protocol for module access --- Pantograph/Protocol.lean | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 62f3f69..c73e791 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -112,6 +112,24 @@ structure ExprEchoResult where type: Expression deriving Lean.ToJson +-- Describe the current state of the environment +structure EnvDescribe where + deriving Lean.FromJson +structure EnvDescribeResult where + imports : Array String + modules : Array String + deriving Lean.ToJson + +-- Describe a module +structure EnvModule where + module : String + deriving Lean.FromJson +structure EnvModuleResult where + imports: Array String + constNames: Array String + extraConstNames: Array String + deriving Lean.ToJson + -- Print all symbols in environment structure EnvCatalog where deriving Lean.FromJson