? is a valid identifier character in Lean.

In particular, this fixes Try This message swapping from the exact?
and apply? tactics, as well as the behavior of `daw` etc.

ftplugin/lean/lean.lua

@@ -3,7 +3,7 @@ vim.b.did_ftplugin = 1
 
 vim.opt.wildignore:append[[*.olean]]
 
-vim.opt_local.iskeyword = [[a-z,A-Z,_,48-57,192-255,!,']]
+vim.opt_local.iskeyword = [[a-z,A-Z,_,48-57,192-255,!,',?]]
 vim.opt_local.comments = [[s0:/-,mb:\ ,ex:-/,:--]]
 vim.opt_local.commentstring=[[/- %s -/]]
 

lua/tests/trythis_spec.lua

@@ -3,7 +3,20 @@ local helpers = require('tests.helpers')
 require('lean').setup {}
 
 describe('trythis', function()
-  it('replaces a single try this', helpers.clean_buffer('lean3', [[
+  it('replaces a single try this', helpers.clean_buffer('lean', [[
+macro "whatshouldIdo?" : tactic => `(tactic| trace "Try this: rfl")
+example : 2 = 2 := by whatshouldIdo?]], function()
+    vim.api.nvim_command('normal G$')
+    helpers.wait_for_line_diagnostics()
+
+    require('lean.trythis').swap()
+    assert.is.same(
+      'example : 2 = 2 := by rfl',
+      vim.api.nvim_get_current_line()
+    )
+  end))
+
+  it('replaces a single try this in lean3', helpers.clean_buffer('lean3', [[
 meta def whatshouldIdo := (do tactic.trace "Try this: existsi 2; refl\n")
 example : ∃ n, n = 2 := by whatshouldIdo]], function()
     vim.api.nvim_command('normal G$')

syntax/lean.vim

@@ -6,7 +6,7 @@
 syn case match
 
 " Valid identifiers (an incomplete list...)
-syn iskeyword a-z,A-Z,_,48-57,192-255,!,.,'
+syn iskeyword a-z,A-Z,_,48-57,192-255,!,.,',?
 
 " keywords