From d6df1ec32fc26524b12bee8eac2ed45fcb4391ed Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 26 Feb 2024 16:15:21 -0800
Subject: [PATCH] fix: register builtin rpc methods (#3512)

---
 src/Lean/Widget/UserWidget.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean
index e534fecfe2..dfd2a537c1 100644
--- a/src/Lean/Widget/UserWidget.lean
+++ b/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