From fd66e70d1e37a245b954d66da2eb87ef1e3b4313 Mon Sep 17 00:00:00 2001
From: "E.W.Ayers" <edward.ayers@outlook.com>
Date: Fri, 10 Jun 2022 13:01:39 -0400
Subject: [PATCH] fix: explicit structure for PPExprTaggedRequest

---
 src/Lean/Server/FileWorker/WidgetRequests.lean | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index b4c343f95e..f33c5d7567 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -17,12 +17,17 @@ import Lean.Server.FileWorker.RequestHandling
 namespace Lean.Widget
 open Server
 
+structure PPExprTaggedRequest where
+  expr : WithRpcRef ExprWithCtx
+  explicit : Bool
+  deriving Inhabited, RpcEncoding
+
 builtin_initialize
   registerBuiltinRpcProcedure
     `Lean.Widget.ppExprTagged
-    (WithRpcRef ExprWithCtx × Bool)
+    PPExprTaggedRequest
     CodeWithInfos
-    fun (⟨ctx, lctx, expr⟩, explicit) => RequestM.asTask do
+    fun ⟨⟨ctx, lctx, expr⟩, explicit⟩ => RequestM.asTask do
       ctx.runMetaM lctx do
         ppExprTagged expr explicit