Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for simultaneous lean3/lean4 (in separate windows/tabs) #35

Closed
wants to merge 75 commits into from
Closed
Changes from 1 commit
Commits
Show all changes
75 commits
Select commit Hold shift + click to select a range
d7e0685
Implement lean3 vs. lean4 filetype detection; remove lean.vim depende…
rish987 Jun 1, 2021
1de6b3b
Fix infoview.
rish987 Jun 1, 2021
cd18592
Fix 4-second lean4 updatetime.
rish987 Jun 2, 2021
d6ea036
Implement multi-tab infoview.
rish987 Jun 2, 2021
70dca5d
Fix infoview toggle.
rish987 Jun 2, 2021
5976501
Index infoviews by windows rather than buffers.
rish987 Jun 2, 2021
23522d4
Update README and add infoview server startup grace period.
rish987 Jun 2, 2021
f15f610
Merge remote-tracking branch 'upstream/main' into main
rish987 Jun 2, 2021
c2db67d
More README notes and add all remaining lean.vim files.
rish987 Jun 2, 2021
f9ac13a
README formatting.
rish987 Jun 2, 2021
edeaa70
Bring syntax files up-to-date, duplicate plugin files from lean to le…
rish987 Jun 3, 2021
81ab591
Remove some lean3 switch mappings from lean4.
rish987 Jun 3, 2021
e6c4656
Update indent file for lean4.
rish987 Jun 3, 2021
50953f9
Remove lean4 executable path stuff from README.
rish987 Jun 3, 2021
7a90e25
Implement dynamically configurable per-tab/per-window option.
rish987 Jun 3, 2021
b9e0576
Slight refactor of infoview.lua.
rish987 Jun 3, 2021
d3ebca1
Fix default one_per_tab setting.
rish987 Jun 3, 2021
0a9a20f
Merge remote-tracking branch 'upstream/main' into main
rish987 Jun 3, 2021
bcef288
Fix some remaining instances of indexing solely by nvim_get_current_w…
rish987 Jun 3, 2021
126690c
Rename src_winnr -> src_idx (readability).
rish987 Jun 3, 2021
5d45699
Get seemingly working auto-infoview-close functionality, but throws e…
rish987 Jun 4, 2021
adf970d
Fix closing single source with multiple source windows in tab in per-…
rish987 Jun 4, 2021
d039630
Refactor autocmds.
rish987 Jun 4, 2021
333c84a
Remove debug print, minor formatting.
rish987 Jun 4, 2021
12e14bd
Fix E855 (per-tab mode error mentioned above) by making an autocmd di…
rish987 Jun 4, 2021
8ade70b
Put back <afile> expansion on WinClosed to avoid any timing issues.
rish987 Jun 5, 2021
5138c58
Remove more begin/ends from Lean 4.
Julian Jun 5, 2021
ef93fa1
pre-commit
Julian Jun 5, 2021
5d1e7a9
Make robust to manual infoview close by user.
rish987 Jun 5, 2021
27dda16
Relocate some refresh_infos() calls.
rish987 Jun 5, 2021
5e024be
Specify whether the infoview is already closed to close_win_wrapper().
rish987 Jun 5, 2021
ba3b226
Make 'lean' filetype refer to Lean 4 and 'lean3' refer to Lean 3.
rish987 Jun 5, 2021
fec293f
Make suggested keymappings buffer-local; make user commands for setti…
rish987 Jun 6, 2021
8e15a8f
Describe suggested mappings in README.
rish987 Jun 6, 2021
6eecae6
Fix abbreviations for lean3/lean4.
rish987 Jun 6, 2021
04d4f60
Revert snippets setting to previous format (accidentally overrode exi…
rish987 Jun 6, 2021
2836a3e
'Fix' compe abbreviations (not sure how to test this).
rish987 Jun 6, 2021
61ff2b6
Fix a minor typo in the README.
Julian Jun 6, 2021
6fca73c
Document the current mappings.
Julian Jun 6, 2021
ff94cd4
Remove the note on LeanPlainGoal.
Julian Jun 6, 2021
28b62d8
Fix automated tests.
rish987 Jun 6, 2021
3265d1b
Merge remote-tracking branch 'upstream/main' into main
rish987 Jun 6, 2021
0c29f2d
Pre-commit
rish987 Jun 6, 2021
bbf811a
Fix README typos.
rish987 Jun 6, 2021
1250a0a
Fix error message when closing infoview after closing source with CTR…
rish987 Jun 6, 2021
1689187
Fix autocmd use of '<buffer=0>'.
rish987 Jun 6, 2021
9f5b875
Add more details to README about new features.
rish987 Jun 6, 2021
22b873b
pre-commit
rish987 Jun 6, 2021
14fbe51
Fix bug where in per-tab mode, closing the 'original' window would ca…
rish987 Jun 6, 2021
7ec6249
Add source comments.
rish987 Jun 6, 2021
0e5d621
Support buffer-local suggested mapping application.
Julian Jun 7, 2021
37be218
Add back the infoview mode-toggling mappings.
Julian Jun 7, 2021
40666a2
Merge branch 'main' into rish
Julian Jun 7, 2021
8885da7
Merge branch 'main' into rish
Julian Jun 7, 2021
e25e07e
Minor readme revert.
Julian Jun 7, 2021
ae3f0bc
Remove some less-relevant notes with the infoview.
Julian Jun 7, 2021
c0b6c0e
Merge branch 'main' into rish
Julian Jun 7, 2021
01f7e35
Merge branch 'main' into rish
Julian Jun 8, 2021
7540117
Minor ternary style, which Lua people seem to like.
Julian Jun 8, 2021
beef5e4
Merge remote-tracking branch 'upstream/main' into main
rish987 Jun 10, 2021
24a4137
Revert a couple ternary refactors and minor close_win_wrapper() fix.
rish987 Jun 10, 2021
d48c9f8
For now, always erase infoviews.
Julian Jun 10, 2021
e73cc6d
Pull in some upstream changes.
Julian Jun 10, 2021
c63b1eb
Remove dead code.
Julian Jun 11, 2021
f97b0a0
Remove some sections from the README.
Julian Jun 11, 2021
1033ed2
Pull in the max_width change.
Julian Jun 11, 2021
0e3e2f6
Pull in the augroup helper
Julian Jun 11, 2021
01d6f99
Use is_lean3_project in _update to detect lean3 projects.
Julian Jun 11, 2021
e3b1063
Guard against lean3ls not existing yet until the PR is merged.
Julian Jun 11, 2021
8604975
Partially pull in teardown.
Julian Jun 11, 2021
ac92804
Remove the note about Lean3 being removed in the future.
Julian Jun 11, 2021
6cb1154
Use lspconfig.util to find leanpkg.toml
Julian Jun 11, 2021
58da940
Get rid of lean3.detect if we already have ft.detect.
Julian Jun 11, 2021
3cdad44
Properly detect leanpkg.toml relative to the lean file, not cwd.
Julian Jun 11, 2021
eb4cd45
Fix infoview closing.
rish987 Jun 11, 2021
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
35 changes: 9 additions & 26 deletions lua/lean/infoview.lua
Original file line number Diff line number Diff line change
Expand Up @@ -38,28 +38,17 @@ local function refresh_infos()
end
end

-- either erase infoview information from table (erase=true)
-- or indicate it has been closed (erase=false)
local function close_win_raw(src_idx, erase)
if erase then M._infoviews_open[src_idx] = nil else M._infoviews_open[src_idx] = false end
M._infoviews[src_idx] = nil

-- necessary because closing a window can cause others to resize
refresh_infos()
end

-- physically close infoview, then either erase it or mark it as closed
local function close_win(src_idx, erase)
-- physically close infoview, then erase it
local function close_win(src_idx)
if M._infoviews[src_idx] then
vim.api.nvim_win_close(M._infoviews[src_idx].win, true)
end

-- NOTE: it seems this isn't necessary since unlisted buffers are deleted automatically?
--if M._infoviews[src_win].buf then
-- vim.api.nvim_buf_delete(M._infoviews[src_win].buf, { force = true })
--end
M._infoviews_open[src_idx] = nil
M._infoviews[src_idx] = nil

close_win_raw(src_idx, erase)
-- necessary because closing a window can cause others to resize
refresh_infos()
end

-- create autocmds under the specified group and local to
Expand Down Expand Up @@ -257,13 +246,7 @@ function M.close_win_wrapper(src_winnr, src_tabnr, close_info, already_closed)
end
end

if close_info then
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The removal of this distinction results in E855: Autocommands caused commands to abort when closing the last (Lean) window in a tab with :close - I don't think WinClosed is designed to be able to handle physically closing other windows. From :help QuitPre: Can be used to close any non-essential window if the current window is the last ordinary window. No similar support exists for WinClosed.

-- if closing with :q, close the infoview as well
close_win(src_idx, true)
else
-- if closing with ctrl-W + c, just detach the infoview and leave it there
close_win_raw(src_idx, true)
end
close_win(src_idx)
end

function M.is_open()
Expand Down Expand Up @@ -295,7 +278,7 @@ end
function M.close_all()
-- close all current infoviews
for key, _ in pairs(M._infoviews) do
close_win(key, false)
close_win(key)
end
for key, _ in pairs(M._infoviews_open) do
M._infoviews_open[key] = nil
Expand All @@ -305,7 +288,7 @@ end
function M.close()
if not M.is_open() then return end

close_win(get_idx(), false)
close_win(get_idx())
end

function M.toggle()
Expand Down