diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 9e6a39479b..033e9cea05 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -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 diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean index c572774aaf..4b137e0459 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -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 ← diff --git a/src/Lean/Widget/Types.lean b/src/Lean/Widget/Types.lean index 1c78dfd763..0fa201a77f 100644 --- a/src/Lean/Widget/Types.lean +++ b/src/Lean/Widget/Types.lean @@ -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 diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index fa5e0c4c59..7f073e0ac1 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -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