Add support for conv? widgets.

Author: Julian

demos/project/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "537a98e0c053976429d5fe61d843c5c8ac2c892e",
+   "rev": "30ae5addc4aba5803b38de4777e03f3a720a9dea",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9f34f4e523881779f8ba46c394c28571c4999db7",
+   "rev": "795ab4977cc1b41273258b736585b9b3def9081c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lua/lean/widgets/ConvSelectionPanel.lua

@@ -0,0 +1,19 @@
+---@brief [[
+---  The `conv?` Mathlib widget.
+---
+--- (It's not namespaced, so it shows up here "globally".)
+---@brief ]]
+
+local Html = require 'proofwidgets.html'
+local widgets = require 'lean.widgets'
+
+---The `conv?` Mathlib widget.
+---@param ctx RenderContext
+---@param params PanelWidgetProps
+return widgets.panel(function(ctx, params)
+  local response, err = ctx:rpc_call('ConvSelectionPanel.rpc', params)
+  if err then
+    return err
+  end
+  return Html(response, ctx)
+end)

lua/proofwidgets/html.lua

@@ -2,6 +2,7 @@ local inductive = require 'std.inductive'
 
 local Element = require('lean.tui').Element
 local InteractiveCode = require 'lean.widget.interactive_code'
+local MakeEditLink = require 'proofwidgets.make_edit_link'
 local Tag = require('tui.html').Tag
 
 ---@class HtmlElement
@@ -43,6 +44,8 @@ local Html = inductive('Html', {
           Element:new { children = children },
         },
       }
+    elseif props.edit then
+      return MakeEditLink(props, children, ctx)
     end
 
     return Element:new {

lua/proofwidgets/make_edit_link.lua

@@ -0,0 +1,54 @@
+local position_to_byte0 = require('std.lsp').position_to_byte0
+
+local Element = require('lean.tui').Element
+
+local hl_ns = vim.api.nvim_create_namespace 'proofwidgets.make_edit_link'
+
+---@class MakeEditLinkProps
+---@field edit lsp.TextDocumentEdit The edit to perform on the file.
+---@field newSelection? lsp.Range Which textual range to select after the edit.
+---                               The range is interpreted in the file that `edit` applies to.
+---                               If present and `start == end`, the cursor is moved to `start`
+---                               and nothing is selected.
+---                               If not present, the selection is not changed.
+---@field title? string
+
+---@param props MakeEditLinkProps
+---@param children Element[]
+---@param ctx RenderContext
+return function(props, children, ctx)
+  return Element:new {
+    children = children,
+    highlightable = true,
+    hlgroup = 'widgetLink',
+    events = {
+      click = function()
+        local bufnr = vim.uri_to_bufnr(props.edit.textDocument.uri)
+        if not vim.api.nvim_buf_is_loaded(bufnr) then
+          return
+        end
+        vim.lsp.util.apply_text_document_edit(props.edit, nil, 'utf-16')
+        if props.newSelection then
+          local start = position_to_byte0(props.newSelection.start, bufnr)
+          if vim.deep_equal(props.newSelection.start, props.newSelection['end']) then
+            local last_window = ctx.get_last_window()
+            if not last_window then
+              return
+            end
+            last_window:make_current()
+            last_window:set_cursor(start)
+          else
+            vim.hl.range(
+              bufnr,
+              hl_ns,
+              'widgetChangedText',
+              start,
+              position_to_byte0(props.newSelection['end'], bufnr),
+              { timeout = 1000 }
+            )
+          end
+        end
+      end,
+    },
+  }
+end

lua/tui/html.lua

@@ -36,7 +36,7 @@ function html.Tag.div(children)
     text = '\n', -- TODO: clearly this isn't fully "block" element-y
     children = {
       Element:new { children = children },
-      Element:new { text = '\n' },
+      -- Element:new { text = '\n' },
     },
   }
 end

spec/fixtures/example-project/lake-manifest.json

@@ -1,7 +1,17 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/ProofWidgets4",
+ [{"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "30ae5addc4aba5803b38de4777e03f3a720a9dea",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
@@ -28,14 +38,54 @@
    "inherited": false,
    "dir": "foo",
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "304c5e2f490d546134c06bf8919e13b175272084",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "25078369972d295301f5a1e53c3e5850cf6d9d4c",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "76a782b161da3faacc43aa5471bbd2e1d262970a",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "36ce5e17d6ab3c881e0cb1bb727982507e708130",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cb53cd3f2958ee503f97ea6162929cabaf96bde9",
+   "rev": "795ab4977cc1b41273258b736585b9b3def9081c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.20.0-rc2",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",

spec/fixtures/example-project/lakefile.toml

@@ -13,5 +13,9 @@ scope = "leanprover-community"
 name = "proofwidgets"
 scope = "leanprover-community"
 
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
+
 [[lean_lib]]
 name = "Test"

spec/widgets/mathlib_spec.lua

@@ -0,0 +1,53 @@
+---@brief [[
+--- Tests for widgets from Mathlib.
+---@brief ]]
+
+local helpers = require 'spec.helpers'
+local infoview = require 'lean.infoview'
+
+require('lean').setup {}
+
+describe('Mathlib widgets', function()
+  it(
+    'supports conv? widgets',
+    helpers.clean_buffer(
+      [[
+      import Mathlib.Tactic.Widget.Conv
+
+      example {n : Nat} : n = n := by
+        conv?
+    ]],
+      function()
+        helpers.search 'conv?'
+        assert.infoview_contents.are [[
+        n : Nat
+        ⊢ n = n
+
+        Nothing selected. You can use gK in the infoview to select expressions in the goal.
+      ]]
+
+        infoview.go_to()
+        helpers.feed 'gK'
+
+        assert.infoview_contents.are [[
+        n : Nat
+        ⊢ n = n
+
+        ▼ Conv 🔍
+        Generate conv
+      ]]
+
+        helpers.search 'Generate'
+        helpers.feed '<CR>'
+
+        assert.infoview_contents.are [[
+        n : Nat
+        | n = n
+      ]]
+
+        -- We've jumped to the Lean window.
+        assert.current_line.is '  conv =>'
+      end
+    )
+  )
+end)