Merge pull request #306 from gihanmarasingha/sorryfill

sorryfill modification for Lean 4

lua/lean/sorry.lua

@@ -4,32 +4,43 @@ local sorry = {}
 
 local function calculate_indent(line)
   local indent = vim.fn.indent(line)
+
   if indent == 0 then
     indent = vim.fn.indent(vim.fn.prevnonblank(line))
   end
-  -- This also doesn't really respect 'expandtab...
+
+  if vim.bo.filetype ~= "lean3" then
+    local line_text = vim.fn.getline(line):gsub("^%s*", "")
+    if line_text:sub(1, 2) == "\194\183" then
+      indent = indent + 2
+    end
+  end
+
   return string.rep(' ', indent)
 end
 
 --- Fill the current cursor position with `sorry`s to discharge all goals.
----
---- I.e., given 3 current goals, with 2 in front of the cursor, will insert:
----      { foo },<cursor>
----      { sorry },
----      { sorry },
 function sorry.fill()
   local params = vim.lsp.util.make_position_params()
   local responses = vim.lsp.buf_request_sync(0, '$/lean/plainGoal', params)
 
+  local sorrytext, offset
+  if vim.bo.filetype == "lean3" then
+      sorrytext = "{ sorry },"
+      offset = 2
+  else
+      sorrytext = "· sorry"
+      offset = 3
+  end
   for _, response in pairs(responses) do
     if not response.result or not response.result.goals or vim.tbl_isempty(response.result.goals) then return end
     local goals = #response.result.goals
     if goals then
       local index = vim.api.nvim_win_get_cursor(0)[1]
       local indent = calculate_indent(index)
-      local lines = tbl_repeat(indent .. "{ sorry },", goals)
+      local lines = tbl_repeat(indent .. sorrytext, goals)
       vim.api.nvim_buf_set_lines(0, index, index, true, lines)
-      vim.api.nvim_win_set_cursor(0, { index + 1, #indent + 2 })  -- the 's'
+      vim.api.nvim_win_set_cursor(0, { index + 1, #indent + offset })  -- the 's'
       return
     end
   end

lua/tests/sorry_spec.lua

@@ -4,7 +4,7 @@ local clean_buffer = helpers.clean_buffer
 require('lean').setup {}
 
 describe('sorry', function()
-  it('inserts sorries for each remaining goal', clean_buffer("lean3", [[
+  it('lean3 inserts sorries for each remaining goal', clean_buffer("lean3", [[
 def foo (n : nat) : n = n := begin
   induction n with d hd,
 end]], function()
@@ -21,7 +21,22 @@ def foo (n : nat) : n = n := begin
 end]]
   end))
 
-  it('leaves the cursor in the first sorry', clean_buffer("lean3", [[
+  it('lean inserts sorries for each remaining goal', clean_buffer('lean', [[
+example (p q : Prop) : p ∧ q ↔ q ∧ p := by
+  constructor]],
+  function()
+    helpers.wait_for_line_diagnostics()
+
+    vim.api.nvim_command('normal! 2gg$')
+    require('lean.sorry').fill()
+    assert.contents.are[[
+example (p q : Prop) : p ∧ q ↔ q ∧ p := by
+  constructor
+  · sorry
+  · sorry]]
+  end))
+
+  it('lean3 leaves the cursor in the first sorry', clean_buffer("lean3", [[
 def foo (n : nat) : n = n := begin
   induction n with d hd,
 end]], function()
@@ -39,7 +54,23 @@ def foo (n : nat) : n = n := begin
 end]]
   end))
 
-  it('indents sorry blocks when needed',
+
+  it('lean leaves the cursor in the first sorry', clean_buffer("lean", [[
+def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by
+  constructor]], function()
+    helpers.wait_for_line_diagnostics()
+
+    vim.api.nvim_command('normal! 2gg$')
+    require('lean.sorry').fill()
+    vim.api.nvim_command('normal! cebar')
+    assert.contents.are[[
+def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by
+  constructor
+  · bar
+  · sorry]]
+  end))
+
+  it('lean3 indents sorry blocks when needed',
     clean_buffer("lean3", [[
 def foo (n : nat) : n = n := begin
   induction n with d hd,
@@ -59,7 +90,27 @@ def foo (n : nat) : n = n := begin
 end]]
   end))
 
-  it('does nothing if there are no goals', clean_buffer("lean3", [[
+  it('lean indents sorry blocks when needed',
+    clean_buffer("lean", [[
+def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by
+  constructor
+
+]], function()
+    vim.api.nvim_command('normal! gg$')
+    helpers.wait_for_line_diagnostics()
+
+    vim.api.nvim_command('normal! 3gg0')
+    require('lean.sorry').fill()
+    assert.contents.are[[
+def foo (p q : Prop) : p ∧ q ↔ q ∧ p := by
+  constructor
+
+  · sorry
+  · sorry
+]]
+  end))
+
+  it('lean3 does nothing if there are no goals', clean_buffer("lean3", [[
 def foo (n : nat) : n = n := begin
   refl,
 end]], function()
@@ -70,4 +121,15 @@ def foo (n : nat) : n = n := begin
   refl,
 end]]
   end))
+
+
+  it('lean does nothing if there are no goals', clean_buffer("lean", [[
+def foo (n : Nat) : n = n := by
+  rfl]], function()
+    vim.api.nvim_command('normal! 2gg$')
+    require('lean.sorry').fill()
+    assert.contents.are[[
+def foo (n : Nat) : n = n := by
+  rfl]]
+  end))
 end)