feat: widget messages (#4254)
Allows embedding user widgets in structured messages. Companion PR is leanprover/vscode-lean4#449. Some technical choices: - The `MessageData.ofWidget` constructor might not be strictly necessary as we already have `MessageData.ofFormatWithInfos`, and there is `Info.ofUserWidget`. However, `.ofUserWidget` also requires a `Syntax` object (as it is normally produced when widgets are saved at a piece of syntax during elaboration) which we do not have in this case. More generally, it continues to be a bit cursed that `Elab.Info` nodes are used both for elaboration and delaboration (pretty-printing), so entrenching that approach seems wrong. The better approach would be to have a separate notion of pretty-printer annotation; but such a refactor would not be clearly beneficial right now. - To support non-JS-based environments such as https://github.com/Julian/lean.nvim, `.ofWidget` requires also providing another message which approximates the widget in a textual form. However, in practice these environments might still want to support a few specific user widgets such as "Try this". --- Closes #2064.
This commit is contained in:
Wojciech Nawrocki
GitHub
parent
cc33c39cb0
commit
ec59e7a2c0
4 changed files with 73 additions and 34 deletions
|
|
@ -57,23 +57,33 @@ inductive MessageData where
|
|||
This constructor is inspected in various hacks. -/
|
||||
| ofFormatWithInfos : FormatWithInfos → MessageData
|
||||
| ofGoal : MVarId → MessageData
|
||||
/-- A widget instance.
|
||||
|
||||
In `ofWidget wi alt`,
|
||||
the nested message `alt` should approximate the contents of the widget
|
||||
without itself using `ofWidget wi _`.
|
||||
This is used as fallback in environments that cannot display user widgets.
|
||||
`alt` may nest any structured message,
|
||||
for example `ofGoal` to approximate a tactic state widget,
|
||||
and, if necessary, even other widget instances
|
||||
(for which approximations are computed recursively). -/
|
||||
| ofWidget : Widget.WidgetInstance → MessageData → MessageData
|
||||
/-- `withContext ctx d` specifies the pretty printing context `(env, mctx, lctx, opts)` for the nested expressions in `d`. -/
|
||||
| withContext : MessageDataContext → MessageData → MessageData
|
||||
| withNamingContext : NamingContext → MessageData → MessageData
|
||||
/-- Lifted `Format.nest` -/
|
||||
| nest : Nat → MessageData → MessageData
|
||||
| nest : Nat → MessageData → MessageData
|
||||
/-- Lifted `Format.group` -/
|
||||
| group : MessageData → MessageData
|
||||
| group : MessageData → MessageData
|
||||
/-- Lifted `Format.compose` -/
|
||||
| compose : MessageData → MessageData → MessageData
|
||||
| compose : MessageData → MessageData → MessageData
|
||||
/-- Tagged sections. `Name` should be viewed as a "kind", and is used by `MessageData` inspector functions.
|
||||
Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/
|
||||
| tagged : Name → MessageData → MessageData
|
||||
| trace (data : TraceData) (msg : MessageData) (children : Array MessageData)
|
||||
/-- A lazy message.
|
||||
The provided thunk will not be run until it is about to be displayed.
|
||||
This can save computation in cases where the message may never be seen,
|
||||
e.g. when nested inside a collapsed trace.
|
||||
This can save computation in cases where the message may never be seen.
|
||||
|
||||
The `Dynamic` value is expected to be a `MessageData`,
|
||||
which is a workaround for the positivity restriction.
|
||||
|
|
@ -160,6 +170,7 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
|
|||
| _, _, ofFormatWithInfos fmt => return fmt.1
|
||||
| _, none, ofGoal mvarId => return "goal " ++ format (mkMVar mvarId)
|
||||
| nCtx, some ctx, ofGoal mvarId => ppGoal (mkPPContext nCtx ctx) mvarId
|
||||
| nCtx, ctx, ofWidget _ d => formatAux nCtx ctx d
|
||||
| nCtx, _, withContext ctx d => formatAux nCtx ctx d
|
||||
| _, ctx, withNamingContext nCtx d => formatAux nCtx ctx d
|
||||
| nCtx, ctx, tagged _ d => formatAux nCtx ctx d
|
||||
|
|
|
|||
|
|
@ -28,15 +28,25 @@ inductive MsgEmbed where
|
|||
| expr : CodeWithInfos → MsgEmbed
|
||||
/-- An interactive goal display. -/
|
||||
| goal : InteractiveGoal → MsgEmbed
|
||||
/-- Some messages (in particular, traces) are too costly to print eagerly. Instead, we allow
|
||||
the user to expand sub-traces interactively. -/
|
||||
/-- A widget instance.
|
||||
|
||||
`alt` is a fallback rendering of the widget
|
||||
that can be shown in standard, non-interactive LSP diagnostics,
|
||||
as well as when user widgets are not supported by the client. -/
|
||||
| widget (wi : Widget.WidgetInstance) (alt : TaggedText MsgEmbed)
|
||||
/-- Some messages (in particular, traces) are too costly to print eagerly.
|
||||
Instead, we allow the user to expand sub-traces interactively. -/
|
||||
| trace (indent : Nat) (cls : Name) (msg : TaggedText MsgEmbed) (collapsed : Bool)
|
||||
(children : StrictOrLazy (Array (TaggedText MsgEmbed)) (WithRpcRef LazyTraceChildren))
|
||||
deriving Inhabited, RpcEncodable
|
||||
|
||||
/-- The `message` field is the text of a message possibly containing interactive *embeds* of type
|
||||
`MsgEmbed`. We maintain the invariant that embeds are stored in `.tag`s with empty `.text` subtrees,
|
||||
i.e. `.tag embed (.text "")`, because a `MsgEmbed` display involve more than just text. -/
|
||||
/-- The `message` field is the text of a message
|
||||
possibly containing interactive *embeds* of type `MsgEmbed`.
|
||||
We maintain the invariant that embeds are stored in `.tag`s with empty `.text` subtrees,
|
||||
i.e., `.tag embed (.text "")`.
|
||||
|
||||
Client-side display algorithms render tags in a custom way,
|
||||
ignoring the nested text. -/
|
||||
abbrev InteractiveDiagnostic := Lsp.DiagnosticWith (TaggedText MsgEmbed)
|
||||
|
||||
deriving instance RpcEncodable for Lsp.DiagnosticWith
|
||||
|
|
@ -44,14 +54,15 @@ deriving instance RpcEncodable for Lsp.DiagnosticWith
|
|||
namespace InteractiveDiagnostic
|
||||
open MsgEmbed
|
||||
|
||||
def toDiagnostic (diag : InteractiveDiagnostic) : Lsp.Diagnostic :=
|
||||
partial def toDiagnostic (diag : InteractiveDiagnostic) : Lsp.Diagnostic :=
|
||||
{ diag with message := prettyTt diag.message }
|
||||
where
|
||||
prettyTt (tt : TaggedText MsgEmbed) : String :=
|
||||
let tt : TaggedText MsgEmbed := tt.rewrite fun
|
||||
| .expr tt, _ => .text tt.stripTags
|
||||
| .goal g, _ => .text (toString g.pretty)
|
||||
| .trace .., _ => .text "(trace)"
|
||||
| .expr tt, _ => .text tt.stripTags
|
||||
| .goal g, _ => .text (toString g.pretty)
|
||||
| .widget _ alt, _ => .text $ prettyTt alt
|
||||
| .trace .., _ => .text "(trace)"
|
||||
tt.stripTags
|
||||
|
||||
/-- Compares interactive diagnostics modulo `TaggedText` tags and traces. -/
|
||||
|
|
@ -88,6 +99,8 @@ private inductive EmbedFmt
|
|||
/-- Nested text is ignored. -/
|
||||
| goal (ctx : Elab.ContextInfo) (lctx : LocalContext) (g : MVarId)
|
||||
/-- Nested text is ignored. -/
|
||||
| widget (wi : WidgetInstance) (alt : Format)
|
||||
/-- Nested text is ignored. -/
|
||||
| trace (cls : Name) (msg : Format) (collapsed : Bool)
|
||||
(children : StrictOrLazy (Array Format) (Array MessageData))
|
||||
/-- Nested tags are ignored, show nested text as-is. -/
|
||||
|
|
@ -128,20 +141,23 @@ where
|
|||
}
|
||||
|
||||
go (nCtx : NamingContext) : Option MessageDataContext → MessageData → MsgFmtM Format
|
||||
| none, ofFormatWithInfos ⟨fmt, _⟩ => withIgnoreTags fmt
|
||||
| some ctx, ofFormatWithInfos ⟨fmt, infos⟩ => do
|
||||
| none, ofFormatWithInfos ⟨fmt, _⟩ => withIgnoreTags fmt
|
||||
| some ctx, ofFormatWithInfos ⟨fmt, infos⟩ => do
|
||||
let t ← pushEmbed <| EmbedFmt.code (mkContextInfo nCtx ctx) infos
|
||||
return Format.tag t fmt
|
||||
| none, ofGoal mvarId => pure $ "goal " ++ format (mkMVar mvarId)
|
||||
| some ctx, ofGoal mvarId =>
|
||||
return .tag (← pushEmbed (.goal (mkContextInfo nCtx ctx) ctx.lctx mvarId)) "\n"
|
||||
| _, withContext ctx d => go nCtx ctx d
|
||||
| ctx, withNamingContext nCtx d => go nCtx ctx d
|
||||
| ctx, tagged _ d => go nCtx ctx d
|
||||
| ctx, nest n d => Format.nest n <$> go nCtx ctx d
|
||||
| ctx, compose d₁ d₂ => do let d₁ ← go nCtx ctx d₁; let d₂ ← go nCtx ctx d₂; pure $ d₁ ++ d₂
|
||||
| ctx, group d => Format.group <$> go nCtx ctx d
|
||||
| ctx, .trace data header children => do
|
||||
| none, ofGoal mvarId => pure $ "goal " ++ format (mkMVar mvarId)
|
||||
| some ctx, ofGoal mvarId =>
|
||||
return .tag (← pushEmbed (.goal (mkContextInfo nCtx ctx) ctx.lctx mvarId)) default
|
||||
| ctx, ofWidget wi d => do
|
||||
let t ← pushEmbed <| EmbedFmt.widget wi (← go nCtx ctx d)
|
||||
return Format.tag t default
|
||||
| _, withContext ctx d => go nCtx ctx d
|
||||
| ctx, withNamingContext nCtx d => go nCtx ctx d
|
||||
| ctx, tagged _ d => go nCtx ctx d
|
||||
| ctx, nest n d => Format.nest n <$> go nCtx ctx d
|
||||
| ctx, compose d₁ d₂ => do let d₁ ← go nCtx ctx d₁; let d₂ ← go nCtx ctx d₂; pure $ d₁ ++ d₂
|
||||
| ctx, group d => Format.group <$> go nCtx ctx d
|
||||
| ctx, .trace data header children => do
|
||||
let mut header := (← go nCtx ctx header).nest 4
|
||||
if data.startTime != 0 then
|
||||
header := f!"[{data.stopTime - data.startTime}] {header}"
|
||||
|
|
@ -159,7 +175,7 @@ where
|
|||
else
|
||||
pure (.strict (← children.mapM (go nCtx ctx)))
|
||||
let e := .trace data.cls header data.collapsed nodes
|
||||
return .tag (← pushEmbed e) ".\n"
|
||||
return .tag (← pushEmbed e) default
|
||||
| ctx?, ofLazy f _ => do
|
||||
let dyn ← f (ctx?.map (mkPPContext nCtx))
|
||||
let some msg := dyn.get? MessageData
|
||||
|
|
@ -188,6 +204,8 @@ partial def msgToInteractive (msgData : MessageData) (hasWidgets : Bool) (indent
|
|||
| .goal ctx lctx g =>
|
||||
ctx.runMetaM lctx do
|
||||
return .tag (.goal (← goalToInteractive g)) default
|
||||
| .widget wi alt =>
|
||||
return .tag (.widget wi (← fmtToTT alt col)) default
|
||||
| .trace cls msg collapsed children => do
|
||||
let col := col + tt.stripTags.length - 2
|
||||
let children ←
|
||||
|
|
|
|||
|
|
@ -26,5 +26,6 @@ structure WidgetInstance where
|
|||
so must be stored as a computation
|
||||
with access to the RPC object store. -/
|
||||
props : StateM Server.RpcObjectStore Json
|
||||
deriving Server.RpcEncodable
|
||||
|
||||
end Lean.Widget
|
||||
|
|
|
|||
|
|
@ -214,17 +214,28 @@ def addPanelWidgetLocal [Monad m] [MonadEnv m] (wi : WidgetInstance) : m Unit :=
|
|||
def erasePanelWidget [Monad m] [MonadEnv m] (h : UInt64) : m Unit := do
|
||||
modifyEnv fun env => panelWidgetsExt.modifyState env fun st => st.erase h
|
||||
|
||||
/-- Save the data of a panel widget which will be displayed whenever the text cursor is on `stx`.
|
||||
/-- Construct a widget instance by finding a widget module
|
||||
in the current environment.
|
||||
|
||||
`hash` must be `hash (toModule c).javascript`
|
||||
where `c` is some global constant annotated with `@[widget_module]`. -/
|
||||
def savePanelWidgetInfo (hash : UInt64) (props : StateM Server.RpcObjectStore Json) (stx : Syntax) :
|
||||
CoreM Unit := do
|
||||
where `c` is some global constant annotated with `@[widget_module]`,
|
||||
or the name of a builtin widget module. -/
|
||||
def WidgetInstance.ofHash (hash : UInt64) (props : StateM Server.RpcObjectStore Json) :
|
||||
CoreM WidgetInstance := do
|
||||
let env ← getEnv
|
||||
let builtins ← builtinModulesRef.get
|
||||
let some id :=
|
||||
(builtins.find? hash |>.map (·.1)) <|> (moduleRegistry.getState env |>.find? hash |>.map (·.1))
|
||||
| throwError s!"No widget module with hash {hash} registered"
|
||||
pushInfoLeaf <| .ofUserWidgetInfo { id, javascriptHash := hash, props, stx }
|
||||
return { id, javascriptHash := hash, props }
|
||||
|
||||
/-- Save the data of a panel widget which will be displayed whenever the text cursor is on `stx`.
|
||||
|
||||
`hash` must be as in `WidgetInstance.ofHash`. -/
|
||||
def savePanelWidgetInfo (hash : UInt64) (props : StateM Server.RpcObjectStore Json) (stx : Syntax) :
|
||||
CoreM Unit := do
|
||||
let wi ← WidgetInstance.ofHash hash props
|
||||
pushInfoLeaf <| .ofUserWidgetInfo { wi with stx }
|
||||
|
||||
/-! ## `show_panel_widgets` command -/
|
||||
|
||||
|
|
@ -372,8 +383,6 @@ opaque evalUserWidgetDefinition [Monad m] [MonadEnv m] [MonadOptions m] [MonadEr
|
|||
|
||||
/-! ## Retrieving panel widget instances -/
|
||||
|
||||
deriving instance Server.RpcEncodable for WidgetInstance
|
||||
|
||||
/-- Retrieve all the `UserWidgetInfo`s that intersect a given line. -/
|
||||
def widgetInfosAt? (text : FileMap) (t : InfoTree) (hoverLine : Nat) : List UserWidgetInfo :=
|
||||
t.deepestNodes fun
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue