From 684b8e234bb48fdfaea2f6a9f57e450a7b658f00 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 14 Dec 2023 19:50:42 +0100 Subject: [PATCH] chore: use derive handler --- src/Lean/Widget/UserWidget.lean | 19 +++---------------- 1 file changed, 3 insertions(+), 16 deletions(-) diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index 2f00c4b7e6a85..57fa74048731a 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -7,19 +7,6 @@ Authors: E.W.Ayers, Wojciech Nawrocki import Lean.Elab.Eval import Lean.Server.Rpc.RequestHandling -namespace Lean.Server -open Elab Command in -/-- Derive `Lean.Server.RpcEncodable` for a type. - -TODO: remove after update-stage0 -/ -elab "#mkrpcenc" n:ident : command => do - elabCommand <| ← `( - namespace $n - deriving instance Lean.Server.RpcEncodable for $n - end $n - ) -end Lean.Server - namespace Lean.Widget open Meta Elab @@ -207,7 +194,7 @@ def savePanelWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] /-! ## Retrieving panel widget instances -/ -#mkrpcenc WidgetInstance +deriving instance Server.RpcEncodable for WidgetInstance /-- Retrieve all the `UserWidgetInfo`s that intersect a given line. -/ def widgetInfosAt? (text : FileMap) (t : InfoTree) (hoverLine : Nat) : List UserWidgetInfo := @@ -224,12 +211,12 @@ def widgetInfosAt? (text : FileMap) (t : InfoTree) (hoverLine : Nat) : List User structure PanelWidgetInstance extends WidgetInstance where /-- The syntactic span in the Lean file at which the panel widget is displayed. -/ range? : Option Lsp.Range -#mkrpcenc PanelWidgetInstance + deriving Server.RpcEncodable /-- Output of `getWidgets` RPC.-/ structure GetWidgetsResponse where widgets : Array PanelWidgetInstance -#mkrpcenc GetWidgetsResponse + deriving Server.RpcEncodable open Lean Server RequestM in /-- Get the panel widgets present around a particular position. -/