A compatibility layer aimed at redefining the user widget API in terms of modules and components. New features:

• component props have Lean types
• props can be RpcEncodable
• we distinguish between an arbitrary 'widget module' (any ES module) and a 'widget component', that is a module which can be rendered
• moreover only 'panel widget components' can appear as top-level panels in the infoview

TODO: If the design works out, it could replace the current Lean core definitions.

instance ProofWidgets.instTypeNameExpr : TypeName Lean.Expr

Equations

• ProofWidgets.instTypeNameExpr = ProofWidgets.inst✝

@[inline, reducible]

abbrev ProofWidgets.LazyEncodable (α : Type) : Type

Equations

• ProofWidgets.LazyEncodable α = StateM Lean.Server.RpcObjectStore α

instance ProofWidgets.instRpcEncodableLazyEncodableJson : Lean.Server.RpcEncodable (ProofWidgets.LazyEncodable Lean.Json)

Equations

• ProofWidgets.instRpcEncodableLazyEncodableJson = { rpcEncode := fun fn => fn, rpcDecode := fun j => pure (pure j) }

structure ProofWidgets.ExprWithCtx : Type

• ci : Lean.Elab.ContextInfo
• lctx : Lean.LocalContext
• expr : Lean.Expr

instance ProofWidgets.instTypeNameExprWithCtx : TypeName ProofWidgets.ExprWithCtx

Equations

• ProofWidgets.instTypeNameExprWithCtx = ProofWidgets.inst✝

def ProofWidgets.ExprWithCtx.runMetaM {α : Type} (e : ProofWidgets.ExprWithCtx) (x : Lean.Expr → Lean.MetaM α) : IO α

Equations

• ProofWidgets.ExprWithCtx.runMetaM e x = Lean.Elab.ContextInfo.runMetaM e.ci e.lctx (x e.expr)

def ProofWidgets.ExprWithCtx.save (e : Lean.Expr) : Lean.MetaM ProofWidgets.ExprWithCtx

Equations

• ProofWidgets.ExprWithCtx.save e = do let __do_lift ← Lean.Elab.ContextInfo.save let __do_lift_1 ← Lean.getLCtx pure { ci := __do_lift, lctx := __do_lift_1, expr := e }

def ProofWidgets.«command#mkrpcenc_» : Lean.ParserDescr

Derive Lean.Server.RpcEncodable for a type.

HACK: around https://leanprover.zulipchat.com/#narrow/stream/341532-lean4-dev/topic/Should.20instance.20names.20inherit.20macro.20scopes.3F

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.widgetDefPostfix : Lean.Name

Equations

• ProofWidgets.widgetDefPostfix = `_userWidgetDef

structure ProofWidgets.Module : Type

• javascript : String

  A JS module intended for use in user widgets.

  To initialize this field from an external JS file, use include_str "path"/"to"/"file.js". However beware that this does not register a dependency with Lake, so your Lean module will not automatically be rebuilt when the .js file changes.

A widget module is a unit of source code that can execute in the infoview.

structure ProofWidgets.PanelWidgetInfo : Type

• id : Lean.Name

  Name of the widget_module to show.

• props : ProofWidgets.LazyEncodable Lean.Json
• infoId : Lean.Name

instance ProofWidgets.instTypeNamePanelWidgetInfo : TypeName ProofWidgets.PanelWidgetInfo

Equations

• ProofWidgets.instTypeNamePanelWidgetInfo = ProofWidgets.inst✝

structure ProofWidgets.WidgetInstance : Type

• id : Lean.Name

  Name of the widget_module.

• srcHash : UInt64
• props : ProofWidgets.LazyEncodable Lean.Json
• infoId : Lean.Name

A widget component with a resolved source hash and its props.

instance ProofWidgets.WidgetInstance.instRpcEncodableWidgetInstance : Lean.Server.RpcEncodable ProofWidgets.WidgetInstance

Equations

• One or more equations did not get rendered due to their size.

instance ProofWidgets.WidgetInstance.instFromJsonRpcEncodablePacket : Lean.FromJson ProofWidgets.WidgetInstance.RpcEncodablePacket✝

Equations

• ProofWidgets.WidgetInstance.instFromJsonRpcEncodablePacket = { fromJson? := ProofWidgets.WidgetInstance.fromJsonRpcEncodablePacket✝ }

instance ProofWidgets.WidgetInstance.instToJsonRpcEncodablePacket : Lean.ToJson ProofWidgets.WidgetInstance.RpcEncodablePacket✝

Equations

• ProofWidgets.WidgetInstance.instToJsonRpcEncodablePacket = { toJson := ProofWidgets.WidgetInstance.toJsonRpcEncodablePacket✝ }

structure ProofWidgets.PanelWidgetInstanceextends ProofWidgets.WidgetInstance : Type

• id : Lean.Name
• srcHash : UInt64
• props : ProofWidgets.LazyEncodable Lean.Json
• infoId : Lean.Name
• range? : Option Lean.Lsp.Range

instance ProofWidgets.PanelWidgetInstance.instFromJsonRpcEncodablePacket : Lean.FromJson ProofWidgets.PanelWidgetInstance.RpcEncodablePacket✝

Equations

• ProofWidgets.PanelWidgetInstance.instFromJsonRpcEncodablePacket = { fromJson? := ProofWidgets.PanelWidgetInstance.fromJsonRpcEncodablePacket✝ }

instance ProofWidgets.PanelWidgetInstance.instRpcEncodablePanelWidgetInstance : Lean.Server.RpcEncodable ProofWidgets.PanelWidgetInstance

Equations

• One or more equations did not get rendered due to their size.

instance ProofWidgets.PanelWidgetInstance.instToJsonRpcEncodablePacket : Lean.ToJson ProofWidgets.PanelWidgetInstance.RpcEncodablePacket✝

Equations

• ProofWidgets.PanelWidgetInstance.instToJsonRpcEncodablePacket = { toJson := ProofWidgets.PanelWidgetInstance.toJsonRpcEncodablePacket✝ }

structure ProofWidgets.GetPanelWidgetsParams : Type

• pos : Lean.Lsp.Position

instance ProofWidgets.instFromJsonGetPanelWidgetsParams : Lean.FromJson ProofWidgets.GetPanelWidgetsParams

Equations

• ProofWidgets.instFromJsonGetPanelWidgetsParams = { fromJson? := ProofWidgets.fromJsonGetPanelWidgetsParams✝ }

instance ProofWidgets.instToJsonGetPanelWidgetsParams : Lean.ToJson ProofWidgets.GetPanelWidgetsParams

Equations

• ProofWidgets.instToJsonGetPanelWidgetsParams = { toJson := ProofWidgets.toJsonGetPanelWidgetsParams✝ }

structure ProofWidgets.GetPanelWidgetsResponse : Type

• widgets : Array ProofWidgets.PanelWidgetInstance

instance ProofWidgets.GetPanelWidgetsResponse.instRpcEncodableGetPanelWidgetsResponse : Lean.Server.RpcEncodable ProofWidgets.GetPanelWidgetsResponse

Equations

• One or more equations did not get rendered due to their size.

instance ProofWidgets.GetPanelWidgetsResponse.instFromJsonRpcEncodablePacket : Lean.FromJson ProofWidgets.GetPanelWidgetsResponse.RpcEncodablePacket✝

Equations

• ProofWidgets.GetPanelWidgetsResponse.instFromJsonRpcEncodablePacket = { fromJson? := ProofWidgets.GetPanelWidgetsResponse.fromJsonRpcEncodablePacket✝ }

instance ProofWidgets.GetPanelWidgetsResponse.instToJsonRpcEncodablePacket : Lean.ToJson ProofWidgets.GetPanelWidgetsResponse.RpcEncodablePacket✝

Equations

• ProofWidgets.GetPanelWidgetsResponse.instToJsonRpcEncodablePacket = { toJson := ProofWidgets.GetPanelWidgetsResponse.toJsonRpcEncodablePacket✝ }

def ProofWidgets.customInfosAt? (text : Lean.FileMap) (t : Lean.Elab.InfoTree) (hoverPos : String.Pos) : List Lean.Elab.CustomInfo

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.getPanelWidgets (args : ProofWidgets.GetPanelWidgetsParams) : Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.GetPanelWidgetsResponse)

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.metaWidget : Lean.Widget.UserWidgetDefinition

Equations

• One or more equations did not get rendered due to their size.

def ProofWidgets.savePanelWidgetInfo {m : Type → Type} [Monad m] [Lean.Elab.MonadInfoTree m] [Lean.MonadNameGenerator m] (stx : Lean.Syntax) (id : Lean.Name) (props : ProofWidgets.LazyEncodable Lean.Json) : m Unit

Save the data of a panel widget which will be displayed whenever the text cursor is on stx. id must be the name of a definition annotated with @[widget_module]. See PanelWidgetProps.

Equations

• One or more equations did not get rendered due to their size.