max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: make TryThis work in widget messages (#7610)

Browse source 
This PR adjusts the `TryThis` widget to also work in widget messages
rather than only as a panel widget. It also adds additional
documentation explaining why this change was needed.
This commit is contained in:
Wojciech Nawrocki 2025-04-08 12:01:03 -04:00 • committed by GitHub
parent 1b40c46ab1
commit e6ce55ffd4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 17 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Message.lean
View file

@ -66,7 +66,10 @@ inductive MessageData where
`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). -/
(for which approximations are computed recursively).
Note that unlike with `Widget.savePanelWidgetInfo`,
the infoview will not pass any additional props to the widget instance. -/
| 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

5
src/Lean/Meta/Tactic/TryThis.lean
View file

@ -44,9 +44,10 @@ where `<replacement*>` is a link which will perform the replacement.
@[builtin_widget_module] def tryThisWidget : Widget.Module where
javascript := "
import * as React from 'react';
import { EditorContext } from '@leanprover/infoview';
import { EditorContext, EnvPosContext } from '@leanprover/infoview';
const e = React.createElement;
export default function ({ pos, suggestions, range, header, isInline, style }) {
export default function ({ suggestions, range, header, isInline, style }) {
const pos = React.useContext(EnvPosContext)
const editorConnection = React.useContext(EditorContext)
const defStyle = style || {
className: 'link pointer dim',

7
src/Lean/Widget/Types.lean
View file

@ -21,9 +21,14 @@ structure WidgetInstance where
/-- Hash of the JS source of the widget module. -/
javascriptHash : UInt64
/-- Arguments to be passed to the component's default exported function.
Must be a JSON object.
In certain contexts
(such as when rendering as a panel widget; see `Widget.savePanelWidgetInfo`),
the Lean infoview appends additional fields to this object.
Props may contain RPC references,
so must be stored as a computation
so must be stored as a `StateM` computation
with access to the RPC object store. -/
props : StateM Server.RpcObjectStore Json
deriving Server.RpcEncodable

5
src/Lean/Widget/UserWidget.lean
View file

@ -231,7 +231,10 @@ def WidgetInstance.ofHash (hash : UInt64) (props : StateM Server.RpcObjectStore
/-- 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`. -/
`hash` must be as in `WidgetInstance.ofHash`.
For panel widgets, the Lean infoview appends additional fields to the `props` object:
see https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/userWidget.tsx#L145. -/
def savePanelWidgetInfo (hash : UInt64) (props : StateM Server.RpcObjectStore Json) (stx : Syntax) :
CoreM Unit := do
let wi ← WidgetInstance.ofHash hash props