From 3667b46d1e301009cf8776adb1d3ebbbae0b84af Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 13 Aug 2021 18:19:36 -0400 Subject: [PATCH] chore: support goals embedded in messages --- src/Lean/Widget/InteractiveDiagnostic.lean | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean index 4bc85a9fef..9bfb680e17 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -29,22 +29,25 @@ inductive MsgEmbed where namespace MsgEmbed --- TODO(WN): `deriving RpcEncoding` for `inductive` +-- TODO(WN): `deriving RpcEncoding` for `inductive` to replace the following hack +@[reducible] +def rpcPacketFor {β : outParam Type} (α : Type) [RpcEncoding α β] := β + private inductive RpcEncodingPacket where | expr : TaggedText Lsp.RpcRef → RpcEncodingPacket - | goal : Nat → RpcEncodingPacket -- TODO + | goal : rpcPacketFor InteractiveGoal → RpcEncodingPacket | lazyTrace : Nat → Name → Lsp.RpcRef → RpcEncodingPacket deriving Inhabited, FromJson, ToJson instance : RpcEncoding MsgEmbed RpcEncodingPacket where rpcEncode a := match a with | expr t => return RpcEncodingPacket.expr (← rpcEncode t) - | goal t => return RpcEncodingPacket.goal 0 + | goal g => return RpcEncodingPacket.goal (← rpcEncode g) | lazyTrace col n t => return RpcEncodingPacket.lazyTrace col n (← rpcEncode t) rpcDecode a := match a with | RpcEncodingPacket.expr t => return expr (← rpcDecode t) - | RpcEncodingPacket.goal t => return unreachable! + | RpcEncodingPacket.goal g => return goal (← rpcDecode g) | RpcEncodingPacket.lazyTrace col n t => return lazyTrace col n (← rpcDecode t) end MsgEmbed