Try this

Stream: mathlib4

[Johan Commelin]

Can we make "Try this" work in the Lean4 VScode? Maybe there are plans to have a better solution in the future, but I think it's really useful to have a tmp fix as well.

[Johan Commelin]

Doesn't even have to be via the extension. If someone knows how to make it work via some other snippet, or so.

[Heather Macbeth]

I hadn't even realised that it wasn't working! I've had mysterious output before from library_search and abel and I guess that would explain it.

[Mario Carneiro]

I think @Gabriel Ebner should make the call on whether it would be good to introduce a short term solution here

[Wojciech Nawrocki]

In the meantime here is one short-term solution:

import Lean.Widget.UserWidget
open Lean Widget

@[widget]
def tryThisWidget : UserWidgetDefinition where
    name := "Try this"
    javascript := "
        import * as React from 'react'
        import { EditorContext } from '@leanprover/infoview'
        const e = React.createElement

        /**
         * @typedef TryThisProps
         * @type {object}
         * @property {DocumentPosition} pos - where the text cursor is.
         * @property {TextEdit} edit - the edit to apply.
         */
        export default function({pos, edit}) {
            const textDocEdit = {
                textDocument: {
                    uri: pos.uri,
                    version: null
                },
                edits: [edit]
            }
            const ec = React.useContext(EditorContext)
            const aProps = {
                className: 'link pointer dim',
                onClick: () => {
                    const workspaceEdit = {
                        documentChanges: [textDocEdit]
                    }
                    console.log(workspaceEdit)
                    ec.api.applyEdit(workspaceEdit)
                }
            }
            return e('a', aProps, `Try this: ${edit.newText}`)
        }
    "

def Lean.FileMap.utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range where
    start := text.utf8PosToLspPos range.start
    «end» := text.utf8PosToLspPos range.stop

/-- Call this from a tactic or other metaprogram in order to display a "Try this" link in the infoview
when the cursor is on `ref`. When clicked, the link will replace `replaceRef` with `newText`. -/
def saveTryThis (ref : Syntax) (newText : String) (replaceRef := ref) : MetaM Unit := do
    let some range := replaceRef.getRange? |
        throwError "No position associated with syntax '{replaceRef}'. Is it synthetic?"
    let text ← getFileMap
    let textEdit : Lsp.TextEdit := { range := text.utf8RangeToLspRange range, newText }
    logInfo m!"Try this: {newText}"
    saveWidgetInfo
        ``tryThisWidget
        (Json.mkObj [
            ("edit", toJson textEdit)
        ])
        ref

elab "secretlyrfl" : tactic => do
    let ref ← getRef
    saveTryThis ref "rfl"

example : 2 + 2 = 4 := by
    secretlyrfl

[Wojciech Nawrocki]

One issue is that this comes up with a non-clickable message, and a separate yes-clickable panel in the infoview. A proper solution would be good but is a little technically involved (a MessageData.ofWidget constructor).