feat: user widgets

See leanprover#1225

doc/widgets.md

@@ -0,0 +1,58 @@
+# 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
+@[widgetSource]
+def widget1 : String := `
+  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`.
+Here is an example lakefile snippet that sets this up.
+Your npm javascript project lives in a subfolder called `./widget` whose build process generates a single file `widget/dist/index.js`.
+
+```lean
+-- ./lakefile.lean
+
+def jsTarget (pkgDir : FilePath) : FileTarget :=
+  let jsFile := pkgDir / "widget/dist/index.js"
+  let srcFiles := inputFileTarget <| pkgDir / "widget/src/index.tsx"
+  fileTargetWithDep jsFile srcFiles fun _srcFile => do
+    proc {
+      cmd := "npm"
+      args := #["install"]
+      cwd := some <| pkgDir / "widget"
+    }
+    proc {
+      cmd := "npm"
+      args := #["run", "build"]
+      cwd := some <| pkgDir / "widget"
+    }
+
+package MyPackage (pkgDir) {
+  extraDepTarget := jsTarget pkgDir |>.withoutInfo
+  ...
+}
+
+...
+```

src/Lean/Elab/InfoTree.lean

@@ -114,6 +114,23 @@ 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. -/
+  widgetSourceId : Name
+  /-- Json representing the props to be loaded in to the component.
+
+  [todo] how to support Rpc encoding of expressions etc?
+  -/
+  props : Json
+  /-- Hash of the `WidgetSource` code to use. -/
+  hash : String
+  deriving Inhabited
+
 def CustomInfo.format : CustomInfo → Format
   | i => Std.ToFormat.format i.json
 
@@ -127,6 +144,7 @@ inductive Info where
   | ofMacroExpansionInfo (i : MacroExpansionInfo)
   | ofFieldInfo (i : FieldInfo)
   | ofCompletionInfo (i : CompletionInfo)
+  | ofUserWidgetInfo (i : UserWidgetInfo)
   | ofCustomInfo (i : CustomInfo)
   deriving Inhabited
 
@@ -285,13 +303,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.widgetSourceId}\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 +323,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

@@ -119,6 +119,18 @@ 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.TextDocumentPositionParams)
+  (f : Snapshots.Snapshot → RequestM α): RequestM (RequestTask α) := do
+  let doc ← readDoc
+  let pos := doc.meta.text.lspPosToUtf8Pos lspPos.position
+  withWaitFindSnap
+    doc
+    (fun s => s.endPos >= pos)
+    (notFoundX := throw $ RequestError.mk JsonRpc.ErrorCode.invalidRequest s!"no snapshot found at {lspPos}")
+    f
+
 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,170 @@
+/-
+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
+
+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 [tutorial](doc/widgets.md) above this declaration for more information on
+how to use the widgets system.
+
+-/
+structure WidgetSource where
+  /-- Unique identifier for the widget. -/
+  widgetSourceId : Name
+  /-- Sourcetext of the code to run.-/
+  sourcetext : String
+  hash : String := toString $ hash sourcetext
+  deriving Inhabited, ToJson, FromJson
+
+namespace WidgetSource
+
+builtin_initialize widgetSourceRegistry : MapDeclarationExtension WidgetSource ← mkMapDeclarationExtension `widgetSourceRegistry
+
+private unsafe def attributeImplUnsafe : AttributeImpl where
+  name := `widgetSource
+  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 value ← evalConstCheck String ``String decl
+    setEnv <| widgetSourceRegistry.insert env decl {widgetSourceId := decl, sourcetext := value}
+
+@[implementedBy attributeImplUnsafe]
+opaque attributeImpl : AttributeImpl
+
+/-- Find the WidgetSource for given widget id. -/
+protected def find? (env : Environment) (id : Name) : Option WidgetSource :=
+  widgetSourceRegistry.find? env id
+
+/-- Returns true if the environment contains the given widget id. -/
+protected def contains (env : Environment) (id : Name) : Bool :=
+  widgetSourceRegistry.contains env id
+
+/-- Gets the hash of the static javascript string for the given widget id, or throws if
+there is no static javascript registered. -/
+def getHash [MonadEnv m] [Monad m] [MonadError m] (id : Name) : m String := do
+  let env ← getEnv
+  let some j := WidgetSource.find? env id | throwError "No code found for {id}."
+  return j.hash
+
+builtin_initialize registerBuiltinAttribute attributeImpl
+
+end WidgetSource
+
+structure GetWidgetSourceParams where
+  widgetSourceId : Name
+  pos : Lean.Lsp.TextDocumentPositionParams
+  deriving ToJson, FromJson
+
+open Lean.Server Lean
+
+open 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 w := WidgetSource.find? env args.widgetSourceId then
+      return w
+    else
+      throw  (RequestError.mk JsonRpc.ErrorCode.invalidParams s!"No registered user-widget with name {args.widgetSourceId}")
+
+open Lean Elab
+
+/--
+  Try to retrieve the `UserWidgetInfo` at a particular position.
+-/
+partial def widgetInfoAt? (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
+
+structure UserWidgetInfoNoStx where
+  widgetSourceId : Name
+  hash : String
+  props : Json
+  -- [todo] you can't toJson syntax yet.
+  -- once we can this class can be deleted and replaced with UserWidgetInfo
+  -- stx : Syntax
+  range? : Option Lsp.Range
+  deriving ToJson, FromJson
+
+structure GetWidgetInfosResponse where
+  infos : Array UserWidgetInfoNoStx
+  deriving ToJson, FromJson
+
+open RequestM in
+/-- Get the UserWidgetInfos present at a particular position. -/
+@[serverRpcMethod]
+def getWidgetInfos (args : Lean.Lsp.TextDocumentPositionParams) : RequestM (RequestTask (GetWidgetInfosResponse)) := do
+  let doc ← readDoc
+  let filemap := doc.meta.text
+  let pos := filemap.lspPosToUtf8Pos args.position
+  withWaitFindSnapAtPos args fun snap => do
+      let ws := widgetInfoAt? filemap snap.infoTree pos
+      let ws := ws.toArray.map (fun w => {
+        widgetSourceId := w.widgetSourceId,
+        hash := w.hash,
+        props := w.props,
+        range? := String.Range.toLspRange filemap <$> Syntax.getRange? w.stx,
+        })
+      return {infos := ws}
+
+/-- Save a user-widget instance to the infotree. -/
+def saveWidgetInfo [Monad m] [MonadEnv m] [MonadError m] [MonadInfoTree m] (widgetSourceId : Name) (props : Json) (stx : Syntax):  m Unit := do
+  let hash ← WidgetSource.getHash widgetSourceId
+  let info := Info.ofUserWidgetInfo {
+    widgetSourceId := widgetSourceId,
+    hash := hash,
+    props := props,
+    stx := stx,
+  }
+  pushInfoLeaf info
+
+/-!
+# Widget command
+
+Use this to place a widget. Useful for debugging widgets.
+-/
+
+syntax (name := widgetCmd) "#widget " ident term : command
+
+private unsafe def  evalJsonUnsafe (stx : Syntax) : TermElabM Json := do
+  let e ← Term.elabTerm stx (mkConst ``Json)
+  let e ← Meta.instantiateMVars e
+  Term.evalExpr Json ``Json e
+
+@[implementedBy evalJsonUnsafe]
+private opaque evalJson (stx : Syntax) : TermElabM Json
+
+open Elab Command in
+@[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
+    return ()
+  | _ => throwUnsupportedSyntax
+
+
+end Lean.Widget