diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 6a1768e1d6..cda2165b51 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -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
diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean
index cc4d7aa5b8..f4867b0129 100644
--- a/src/Lean/Meta/Tactic/TryThis.lean
+++ b/src/Lean/Meta/Tactic/TryThis.lean
@@ -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',
diff --git a/src/Lean/Widget/Types.lean b/src/Lean/Widget/Types.lean
index 0fa201a77f..8a3ce41301 100644
--- a/src/Lean/Widget/Types.lean
+++ b/src/Lean/Widget/Types.lean
@@ -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
diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean
index 04cf13d6cd..3c0d9bd59d 100644
--- a/src/Lean/Widget/UserWidget.lean
+++ b/src/Lean/Widget/UserWidget.lean
@@ -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