chore: use derive handler

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. -/