feat: user widgets

doc/SUMMARY.md

@@ -65,6 +65,7 @@
 - [Frequently Asked Questions](./faq.md)
 - [Significant Changes from Lean 3](./lean3changes.md)
 - [Syntax Highlighting Lean in LaTeX](./syntax_highlight_in_latex.md)
+- [User Widgets](./widgets.md)
 
 # Development
 

doc/widgets.md

@@ -0,0 +1,37 @@
+# The user-widgets system
+
+Proving is an inherently interactive task. Lots of mathematical objects that we use are visual in nature.
+The user-widget system lets users associate React components with the Lean document which are then rendered in the Lean VSCode infoview.
+
+There is nothing about the RPC calls presented here that make the user-widgets system
+dependent on JavaScript. However the primary use case is the web-based infoview in VSCode.
+
+## How to write your own user-widgets
+
+You can write your own user-widgets using the `@[widgetSource]` attribute:
+
+```lean
+import Lean
+open Lean Widget
+
+@[widget]
+def widget1 : UserWidgetDefinition := {
+  name := "my fancy widget"
+  javascript := "
+  import * as React from 'react';
+  export default function (props) {
+    return React.createElement('p', {}, 'hello')
+  }"
+}
+```
+
+This JavaScript text must include `import * as React from "react"` in the imports and may not use JSX.
+The default export of the sourcetext must be a React component whose props are an RPC encoding.
+The React component may accept a props argument whose value will be determined for each particular widget instance (below).
+Widget sources may import the `@lean4/infoview` package ([todo] publish on NPM) in order to use
+components such as `InteractiveMessage` to display `MessageData` interactively.
+
+## Using Lake to build your widgets
+
+For larger projects, you can use Lake to create files that will be used as `widgetSource`.
+To learn how to do this, please view the readme of the [WidgetsMinimal sample](https://github.com/leanprover/lean4-samples/tree/main/WidgetsMinimal) ([todo] merge sample).

src/Lean/Data/Parsec.lean

@@ -55,6 +55,11 @@ def attempt (p : Parsec α) : Parsec α := λ it =>
 instance : Alternative Parsec :=
 { failure := fail "", orElse }
 
+protected def run (p : Parsec α) (s : String) : Except String α :=
+  match p s.mkIterator with
+  | Parsec.ParseResult.success _ res => Except.ok res
+  | Parsec.ParseResult.error it err  => Except.error s!"offset {repr it.i.byteIdx}: {err}"
+
 def expectedEndOfInput := "expected end of input"
 
 @[inline]
@@ -86,6 +91,7 @@ def manyChars (p : Parsec Char) : Parsec String := manyCharsCore p ""
 @[inline]
 def many1Chars (p : Parsec Char) : Parsec String := do manyCharsCore p (←p).toString
 
+/-- Parses the given string. -/
 def pstring (s : String) : Parsec String := λ it =>
   let substr := it.extract (it.forward s.length)
   if substr = s then

src/Lean/Elab/InfoTree.lean

@@ -114,6 +114,18 @@ structure CustomInfo where
   json : Json
   deriving Inhabited
 
+/-- An info that represents a user-widget.
+User-widgets are custom pieces of code that run on the editor client.
+You can learn about user widgets at `src/Lean/Widget/UserWidget`
+-/
+structure UserWidgetInfo where
+  stx : Syntax
+  /-- Id of `WidgetSource` object to use. -/
+  widgetId : Name
+  /-- Json representing the props to be loaded in to the component. -/
+  props : Json
+  deriving Inhabited
+
 def CustomInfo.format : CustomInfo → Format
   | i => Std.ToFormat.format i.json
 
@@ -127,6 +139,7 @@ inductive Info where
   | ofMacroExpansionInfo (i : MacroExpansionInfo)
   | ofFieldInfo (i : FieldInfo)
   | ofCompletionInfo (i : CompletionInfo)
+  | ofUserWidgetInfo (i : UserWidgetInfo)
   | ofCustomInfo (i : CustomInfo)
   deriving Inhabited
 
@@ -285,13 +298,17 @@ def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) :
   let output ← ctx.ppSyntax info.lctx info.output
   return f!"Macro expansion\n{stx}\n===>\n{output}"
 
+def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
+  f!"UserWidget {info.widgetId}\n{Std.ToFormat.format info.props}"
+
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx
   | ofTermInfo i           => i.format ctx
   | ofCommandInfo i        => i.format ctx
   | ofMacroExpansionInfo i => i.format ctx
   | ofFieldInfo i          => i.format ctx
   | ofCompletionInfo i     => i.format ctx
+  | ofUserWidgetInfo i     => pure <| UserWidgetInfo.format i
   | ofCustomInfo i         => pure <| Std.ToFormat.format i
 
 def Info.toElabInfo? : Info → Option ElabInfo
@@ -301,6 +318,7 @@ def Info.toElabInfo? : Info → Option ElabInfo
   | ofMacroExpansionInfo _ => none
   | ofFieldInfo _          => none
   | ofCompletionInfo _     => none
+  | ofUserWidgetInfo _     => none
   | ofCustomInfo _         => none
 
 /--

src/Lean/Server/InfoUtils.lean

@@ -90,6 +90,7 @@ def Info.stx : Info → Syntax
   | ofFieldInfo i          => i.stx
   | ofCompletionInfo i     => i.stx
   | ofCustomInfo i         => i.stx
+  | ofUserWidgetInfo i     => i.stx
 
 def Info.lctx : Info → LocalContext
   | Info.ofTermInfo i  => i.lctx

src/Lean/Server/Requests.lean

@@ -37,6 +37,9 @@ def methodNotFound (method : String) : RequestError :=
   { code := ErrorCode.methodNotFound
     message := s!"No request handler found for '{method}'" }
 
+def internalError (message : String) : RequestError :=
+  { code := ErrorCode.internalError, message := message }
+
 instance : Coe IO.Error RequestError where
   coe e := { code := ErrorCode.internalError
              message := toString e }
@@ -119,6 +122,37 @@ def bindWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool)
   let findTask ← doc.cmdSnaps.waitFind? p
   bindTask findTask <| waitFindSnapAux notFoundX x
 
+/-- Helper for running an Rpc request at a particular snapshot. -/
+def withWaitFindSnapAtPos
+  (lspPos : Lean.Lsp.Position)
+  (f : Snapshots.Snapshot → RequestM α): RequestM (RequestTask α) := do
+  let doc ← readDoc
+  let pos := doc.meta.text.lspPosToUtf8Pos lspPos
+  withWaitFindSnap
+    doc
+    (fun s => s.endPos >= pos)
+    (notFoundX := throw <| RequestError.mk .invalidParams s!"no snapshot found at {lspPos}")
+    f
+
+open Lean Elab Command in
+/-- Use the command state in the given snapshot to run a `CommandElabM`.-/
+def runCommand (snap : Snapshots.Snapshot) (c : CommandElabM α) : RequestM α := do
+  let r ← read
+  let ctx : Command.Context := {
+    fileName := r.doc.meta.uri,
+    fileMap := r.doc.meta.text,
+    tacticCache? := snap.tacticCache,
+  }
+  let ea ← c.run ctx |>.run snap.cmdState |> EIO.toIO'
+  match ea with
+  | Except.ok (a, _s) => return a
+  | Except.error ex => do
+    throw <| RequestError.internalError <|← ex.toMessageData.toString
+
+/-- Run a `CoreM` using the data in the given snapshot.-/
+def runCore (snap : Snapshots.Snapshot) (c : CoreM α) : RequestM α :=
+  runCommand snap <| Lean.Elab.Command.liftCoreM c
+
 end RequestM
 
 /- The global request handlers table. -/

src/Lean/Widget.lean

@@ -8,3 +8,4 @@ import Lean.Widget.InteractiveCode
 import Lean.Widget.InteractiveDiagnostic
 import Lean.Widget.InteractiveGoal
 import Lean.Widget.TaggedText
+import Lean.Widget.UserWidget

src/Lean/Widget/UserWidget.lean

@@ -0,0 +1,193 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Authors: E.W.Ayers
+-/
+import Lean.Widget.Basic
+import Lean.Data.Json
+import Lean.Environment
+import Lean.Server
+import Lean.Elab.Eval
+
+open Lean
+
+namespace Lean.Widget
+
+/-- A custom piece of code that is run on the editor client.
+
+The editor can use the `Lean.Widget.getWidgetSource` RPC method to
+get this object.
+
+See the [manual entry](doc/widgets.md) above this declaration for more information on
+how to use the widgets system.
+
+-/
+structure WidgetSource where
+  /-- Sourcetext of the code to run.-/
+  sourcetext : String
+  deriving Inhabited, ToJson, FromJson
+
+/-- Use this structure and the `@[widget]` attribute to define your own widgets.
+
+```lean
+@[widget]
+def rubiks : UserWidgetDefinition :=
+  { name := "Rubiks cube app"
+    javascript := include_str ...
+  }
+```
+-/
+structure UserWidgetDefinition where
+  /-- Pretty name of user widget to display to the user. -/
+  name : String
+  /-- An ESmodule that exports a react component to render. -/
+  javascript: String
+  deriving Inhabited, ToJson, FromJson
+
+structure UserWidget where
+  id : Name
+  /-- Pretty name of widget to display to the user.-/
+  name : String
+  javascriptHash: UInt64
+  deriving Inhabited, ToJson, FromJson
+
+private abbrev WidgetSourceRegistry := SimplePersistentEnvExtension
+    (UInt64 × Name)
+    (Std.RBMap UInt64 Name compare)
+
+-- Mapping widgetSourceId to hash of sourcetext
+builtin_initialize userWidgetRegistry : MapDeclarationExtension UserWidget ← mkMapDeclarationExtension `widgetRegistry
+builtin_initialize widgetSourceRegistry : WidgetSourceRegistry ←
+  registerSimplePersistentEnvExtension {
+    name          := `widgetSourceRegistry
+    addImportedFn := fun xss => xss.foldl (Array.foldl (fun s n => s.insert n.1 n.2)) ∅
+    addEntryFn    := fun s n => s.insert n.1 n.2
+    toArrayFn     := fun es => es.toArray
+  }
+
+private unsafe def getUserWidgetDefinitionUnsafe
+  (decl : Name) : CoreM UserWidgetDefinition :=
+  evalConstCheck UserWidgetDefinition ``UserWidgetDefinition decl
+
+@[implementedBy getUserWidgetDefinitionUnsafe]
+private opaque getUserWidgetDefinition
+  (decl : Name) : CoreM UserWidgetDefinition
+
+private def attributeImpl : AttributeImpl where
+  name := `widget
+  descr := "Mark a string as static code that can be loaded by a widget handler."
+  applicationTime := AttributeApplicationTime.afterCompilation
+  add decl _stx _kind := do
+    let env ← getEnv
+    let defn ← getUserWidgetDefinition decl
+    let javascriptHash := hash defn.javascript
+    let env := userWidgetRegistry.insert env decl {id := decl, name := defn.name, javascriptHash}
+    let env := widgetSourceRegistry.addEntry env (javascriptHash, decl)
+    setEnv <| env
+
+builtin_initialize registerBuiltinAttribute attributeImpl
+
+/-- Input for `getWidgetSource` RPC. -/
+structure GetWidgetSourceParams where
+  /-- The hash of the sourcetext to retrieve. -/
+  hash: UInt64
+  pos : Lean.Lsp.Position
+  deriving ToJson, FromJson
+
+open Lean.Server Lean RequestM in
+@[serverRpcMethod]
+def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) :=
+  RequestM.withWaitFindSnapAtPos args.pos fun snap => do
+    let env := snap.cmdState.env
+    if let some id := widgetSourceRegistry.getState env |>.find? args.hash then
+      let d ← Lean.Server.RequestM.runCore snap <| getUserWidgetDefinition id
+      return {sourcetext := d.javascript}
+    else
+      throw <| RequestError.mk .invalidParams s!"No registered user-widget with hash {args.hash}"
+
+open Lean Elab
+
+/--
+  Try to retrieve the `UserWidgetInfo` at a particular position.
+-/
+def widgetInfosAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List UserWidgetInfo :=
+  t.deepestNodes fun
+    | _ctx, i@(Info.ofUserWidgetInfo wi), _cs => do
+      if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
+        let trailSize := i.stx.getTrailingSize
+        -- show info at EOF even if strictly outside token + trail
+        let atEOF := tailPos.byteIdx + trailSize == text.source.endPos.byteIdx
+        guard <| pos ≤ hoverPos ∧ (hoverPos.byteIdx < tailPos.byteIdx + trailSize || atEOF)
+        return wi
+      else
+        failure
+    | _, _, _ => none
+
+/-- UserWidget accompanied by component props. -/
+structure UserWidgetInstance extends UserWidget where
+  /-- Arguments to be fed to the widget's main component. -/
+  props : Json
+  /-- The location of the widget instance in the Lean file. -/
+  range? : Option Lsp.Range
+  deriving ToJson, FromJson
+
+/-- Output of `getWidgets` RPC.-/
+structure GetWidgetsResponse where
+  widgets : Array UserWidgetInstance
+  deriving ToJson, FromJson
+
+open Lean Server RequestM in
+/-- Get the `UserWidget`s present at a particular position. -/
+@[serverRpcMethod]
+def getWidgets (args : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do
+  let doc ← readDoc
+  let filemap := doc.meta.text
+  let pos := filemap.lspPosToUtf8Pos args
+  withWaitFindSnapAtPos args fun snap => do
+    let env := snap.env
+    let ws := widgetInfosAt? filemap snap.infoTree pos
+    let ws ← ws.toArray.mapM (fun (w : UserWidgetInfo) => do
+      let some widget := userWidgetRegistry.find? env w.widgetId
+        | throw <| RequestError.mk .invalidParams s!"No registered user-widget with id {w.widgetId}"
+      return {
+        widget with
+        props := w.props
+        range? := String.Range.toLspRange filemap <$> Syntax.getRange? w.stx
+      })
+    return {widgets := ws}
+
+/-- Save a user-widget instance to the infotree.
+    The given `widgetId` should be the declaration name of the widget definition. -/
+def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widgetId : Name) (props : Json) (stx : Syntax):  m Unit := do
+  let info := Info.ofUserWidgetInfo {
+    widgetId := widgetId
+    props := props
+    stx := stx
+  }
+  pushInfoLeaf info
+
+/-!  # Widget command
+
+Use `#widget <widgetname> <props>` to display a widget.
+-/
+
+syntax (name := widgetCmd) "#widget " ident term : command
+
+open Lean Lean.Meta Lean.Elab Lean.Elab.Term in
+private unsafe def evalJsonUnsafe (stx : Syntax) : TermElabM Json :=
+  Lean.Elab.Term.evalTerm Json (mkConst ``Json) stx
+
+@[implementedBy evalJsonUnsafe]
+private opaque evalJson (stx : Syntax) : TermElabM Json
+
+open Elab Command in
+
+/-- Use this to place a widget. Useful for debugging widgets. -/
+@[commandElab widgetCmd] def elabWidgetCmd : CommandElab := fun
+  | stx@`(#widget $id:ident $props) => do
+    let props : Json ← runTermElabM none (fun _ => evalJson props)
+    saveWidgetInfo id.getId props stx
+  | _ => throwUnsupportedSyntax
+
+end Lean.Widget

src/Std/Data/RBMap.lean

@@ -243,6 +243,8 @@ def RBMap (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Type (max
 instance (α : Type u) (β : Type v) (cmp : α → α → Ordering) : EmptyCollection (RBMap α β cmp) :=
   ⟨RBMap.empty⟩
 
+instance (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Inhabited (RBMap α β cmp) := ⟨∅⟩
+
 namespace RBMap
 variable {α : Type u} {β : Type v} {σ : Type w} {cmp : α → α → Ordering}
 

tests/common.sh

@@ -28,7 +28,7 @@ function compile_lean {
 function exec_capture {
     # mvar suffixes like in `?m.123` are deterministic but prone to change on minor changes, so strip them
     # also strip intermittent "building '/nix/store/..." messages
-    LEAN_BACKTRACE=0 "$@" 2>&1 | perl -pe 's/(\?\w)\.[0-9]+/\1/g;s!building '\''/nix/.*\n!!g' > "$f.produced.out"
+    LEAN_BACKTRACE=0 "$@" 2>&1 | perl -pe 's/(\?(\w|_\w+))\.[0-9]+/\1/g;s!building '\''/nix/.*\n!!g' > "$f.produced.out"
 }
 
 # Remark: `${var+x}` is a parameter expansion which evaluates to nothing if `var` is unset, and substitutes the string `x` otherwise.

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -9,15 +9,15 @@ a : α
 ⊢ α
 [Elab.info] command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
   α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
-    [.] `α : some Sort.{?_uniq.311} @ ⟨7, 13⟩-⟨7, 14⟩
+    [.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
     α : Type @ ⟨7, 13⟩-⟨7, 14⟩
   a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
   α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
-    [.] `α : some Sort.{?_uniq.317} @ ⟨7, 13⟩-⟨7, 14⟩
+    [.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
     α : Type @ ⟨7, 13⟩-⟨7, 14⟩
   a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
   Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
-    [.] `Fam2 : some Sort.{?_uniq.319} @ ⟨7, 21⟩-⟨7, 25⟩
+    [.] `Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩
     Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
     α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
       [.] `α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
@@ -27,7 +27,7 @@ a : α
       β : Type @ ⟨7, 28⟩-⟨7, 29⟩
   x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
   β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
-    [.] `β : some Sort.{?_uniq.321} @ ⟨7, 33⟩-⟨7, 34⟩
+    [.] `β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩
     β : Type @ ⟨7, 33⟩-⟨7, 34⟩
   _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩†
   a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
@@ -45,8 +45,8 @@ a : α
     [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
     @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
     [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-    [.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.656]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.657]]]) @ ⟨9, 4⟩-⟨9, 12⟩
-    [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.656]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
+    [.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
+    [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
     α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
     α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
     Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
@@ -57,9 +57,9 @@ a : α
     Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
     [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
     [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-    [.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.688]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.689]]]) @ ⟨10, 4⟩-⟨10, 12⟩
+    [.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
     [.] `n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
-    [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.688]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
+    [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
     Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
     Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
     Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩

tests/lean/forallMetaBounded.lean.expected.out

@@ -1 +1 @@
-Set ?_uniq.1
+Set ?_uniq

tests/lean/interactive/run.lean

@@ -1,12 +1,20 @@
 import Lean.Data.Lsp
+import Lean.Widget
 open Lean
 open Lean.Lsp
 open Lean.JsonRpc
 
+def word : Parsec String :=
+  Parsec.many1Chars <| Parsec.digit <|> Parsec.asciiLetter <|> Parsec.pchar '_'
+
+def ident : Parsec Name := do
+  let head ← word
+  let xs ← Parsec.many1 (Parsec.pchar '.' *> word)
+  return xs.foldl Name.mkStr $ head
+
 partial def main (args : List String) : IO Unit := do
   let uri := s!"file://{args.head!}"
   Ipc.runWith (←IO.appPath) #["--server"] do
-    let hIn ← Ipc.stdin
     let capabilities := {
       textDocument? := some {
         completion? := some {
@@ -28,6 +36,7 @@ partial def main (args : List String) : IO Unit := do
     let mut lastActualLineNo := 0
     let mut versionNo : Nat := 2
     let mut requestNo : Nat := 2
+    let mut rpcSessionId : Option UInt64 := none
     for line in text.splitOn "\n" do
       match line.splitOn "--" with
       | [ws, directive] =>
@@ -69,18 +78,45 @@ partial def main (args : List String) : IO Unit := do
           for diag in diags do
             IO.eprintln (toJson diag.param)
           requestNo := requestNo + 1
+        | "widgets" =>
+          if rpcSessionId.isNone then
+            Ipc.writeRequest ⟨requestNo, "$/lean/rpc/connect",  RpcConnectParams.mk uri⟩
+            let r ← Ipc.readResponseAs requestNo RpcConnected
+            rpcSessionId := some r.result.sessionId
+            requestNo := requestNo + 1
+          let ps : RpcCallParams := {
+            textDocument := {uri := uri},
+            position := pos,
+            sessionId := rpcSessionId.get!,
+            method := `Lean.Widget.getWidgets,
+            params := toJson pos,
+          }
+          Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩
+          let response ← Ipc.readResponseAs requestNo Lean.Widget.GetWidgetsResponse
+          requestNo := requestNo + 1
+          IO.eprintln (toJson response.result)
+          for w in response.result.widgets do
+            let params : Lean.Widget.GetWidgetSourceParams := { pos, hash := w.javascriptHash }
+            let ps : RpcCallParams := {
+              ps with
+              method := `Lean.Widget.getWidgetSource,
+              params := toJson params,
+            }
+            Ipc.writeRequest ⟨requestNo, "$/lean/rpc/call", ps⟩
+            let resp ← Ipc.readResponseAs requestNo Lean.Widget.WidgetSource
+            IO.eprintln (toJson resp.result)
+            requestNo := requestNo + 1
         | _ =>
           let Except.ok params ← pure <| Json.parse params
             | throw <| IO.userError s!"failed to parse {params}"
           let params := params.setObjVal! "textDocument" (toJson { uri := uri : TextDocumentIdentifier })
           -- TODO: correctly compute in presence of Unicode
-          let column := ws.endPos + "--"
           let params := params.setObjVal! "position" (toJson pos)
           IO.eprintln params
           Ipc.writeRequest ⟨requestNo, method, params⟩
           let rec readFirstResponse := do
             match ← Ipc.readMessage with
-            | resp@(Message.response id r) =>
+            | Message.response id r =>
               assert! id == requestNo
               return r
             | Message.notification .. => readFirstResponse

tests/lean/interactive/userWidget.lean

@@ -0,0 +1,15 @@
+import Lean
+open Lean Widget
+
+@[widget]
+def widget1 : UserWidgetDefinition := {
+  name := "my fancy widget"
+  javascript:= "
+  import * as React from 'react';
+  export default function (props) {
+    return React.createElement('p', {}, 'hello')
+  }"
+}
+
+#widget widget1 (Json.mkObj [])
+  --^ widgets

tests/lean/interactive/userWidget.lean.expected.out

@@ -0,0 +1,10 @@
+{"widgets":
+ [{"range":
+   {"start": {"line": 13, "character": 0},
+    "end": {"line": 13, "character": 31}},
+   "props": {},
+   "name": "my fancy widget",
+   "javascriptHash": "2248127894",
+   "id": "widget1"}]}
+{"sourcetext":
+ "\n  import * as React from 'react';\n  export default function (props) {\n    return React.createElement('p', {}, 'hello')\n  }"}