fix: register builtin rpc methods (#3512)

src/Lean/Widget/UserWidget.lean

@@ -126,7 +126,6 @@ structure WidgetSource where
   deriving Inhabited, ToJson, FromJson
 
 open Server RequestM in
-@[server_rpc_method]
 def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := do
   if let some (_, m) := (← builtinModulesRef.get).find? args.hash then
     return .pure { sourcetext := m.javascript }
@@ -143,6 +142,9 @@ def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask Widge
       else
         notFound
 
+builtin_initialize
+  Server.registerBuiltinRpcProcedure ``getWidgetSource _ _ getWidgetSource
+
 /-! ## Storage of panel widget instances -/
 
 inductive PanelWidgetsExtEntry where
@@ -401,7 +403,6 @@ structure GetWidgetsResponse where
 
 open Lean Server RequestM in
 /-- Get the panel widgets present around a particular position. -/
-@[server_rpc_method]
 def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do
   let doc ← readDoc
   let filemap := doc.meta.text
@@ -435,6 +436,9 @@ def getWidgets (pos : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResp
         return { wi with range? := String.Range.toLspRange filemap <$> Syntax.getRange? wi.stx, name? }
       return { widgets := ws' ++ ws }
 
+builtin_initialize
+  Server.registerBuiltinRpcProcedure ``getWidgets _ _ getWidgets
+
 attribute [deprecated Module] UserWidgetDefinition
 
 end Lean.Widget