Skip to content

Commit 99c6a59

Browse files
JulianJulian
committed
Style noise.
1 parent 45fb261 commit 99c6a59

6 files changed

Lines changed: 146 additions & 76 deletions

File tree

‎lua/lean/infoview.lua‎

Lines changed: 93 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -52,8 +52,6 @@ local function is_trace_diagnostic(element)
5252
return element.events and element.events.trace_search
5353
end
5454

55-
56-
5755
---Find the path to the first descendant matching a predicate.
5856
---@param element Element the element to search within
5957
---@param predicate fun(element: Element): boolean?
@@ -343,12 +341,16 @@ function Infoview:move_cursor_to_goal(n)
343341
if goal then
344342
n = n - 1
345343
if n == 0 then
346-
local goal_path = find_descendant_path(root, function(e) return e == goal end, root_path)
344+
local goal_path = find_descendant_path(root, function(e)
345+
return e == goal
346+
end, root_path)
347347
if goal_path then
348348
-- Navigate past the goal prefix (e.g. '⊢ ') to the goal expression.
349349
local expr = goal:children():nth(2)
350350
local target_path = expr
351-
and find_descendant_path(goal, function(e) return e == expr end, goal_path)
351+
and find_descendant_path(goal, function(e)
352+
return e == expr
353+
end, goal_path)
352354
or goal_path
353355
local pos = renderer:buf_position_from_path(target_path)
354356
if pos then
@@ -390,7 +392,9 @@ function Infoview:__suggestion_path(n)
390392
for suggestion in root:filter(is_suggestion) do
391393
n = n - 1
392394
if n == 0 then
393-
return find_descendant_path(root, function(e) return e == suggestion end, root_path)
395+
return find_descendant_path(root, function(e)
396+
return e == suggestion
397+
end, root_path)
394398
end
395399
end
396400
end
@@ -909,23 +913,43 @@ function Info:new(opts)
909913
iv:__goto('prev', is_goal)
910914
end, { desc = 'Move to the previous goal.' })
911915

912-
pin_buffer.keymaps:set('n', '<LocalLeader>g', '<Plug>(LeanInfoviewGoToGoal)',
913-
{ remap = true, desc = 'Move to the first goal.' })
914-
pin_buffer.keymaps:set('n', ']g', '<Plug>(LeanInfoviewNextGoal)',
915-
{ remap = true, desc = 'Move to the next goal.' })
916-
pin_buffer.keymaps:set('n', '[g', '<Plug>(LeanInfoviewPrevGoal)',
917-
{ remap = true, desc = 'Move to the previous goal.' })
916+
pin_buffer.keymaps:set(
917+
'n',
918+
'<LocalLeader>g',
919+
'<Plug>(LeanInfoviewGoToGoal)',
920+
{ remap = true, desc = 'Move to the first goal.' }
921+
)
922+
pin_buffer.keymaps:set(
923+
'n',
924+
']g',
925+
'<Plug>(LeanInfoviewNextGoal)',
926+
{ remap = true, desc = 'Move to the next goal.' }
927+
)
928+
pin_buffer.keymaps:set(
929+
'n',
930+
'[g',
931+
'<Plug>(LeanInfoviewPrevGoal)',
932+
{ remap = true, desc = 'Move to the previous goal.' }
933+
)
918934

919935
pin_buffer.keymaps:set('n', '<Plug>(LeanInfoviewNextHypothesis)', function()
920936
iv:__goto('next', is_hypothesis)
921937
end, { desc = 'Move to the next hypothesis.' })
922938
pin_buffer.keymaps:set('n', '<Plug>(LeanInfoviewPrevHypothesis)', function()
923939
iv:__goto('prev', is_hypothesis)
924940
end, { desc = 'Move to the previous hypothesis.' })
925-
pin_buffer.keymaps:set('n', ']h', '<Plug>(LeanInfoviewNextHypothesis)',
926-
{ remap = true, desc = 'Move to the next hypothesis.' })
927-
pin_buffer.keymaps:set('n', '[h', '<Plug>(LeanInfoviewPrevHypothesis)',
928-
{ remap = true, desc = 'Move to the previous hypothesis.' })
941+
pin_buffer.keymaps:set(
942+
'n',
943+
']h',
944+
'<Plug>(LeanInfoviewNextHypothesis)',
945+
{ remap = true, desc = 'Move to the next hypothesis.' }
946+
)
947+
pin_buffer.keymaps:set(
948+
'n',
949+
'[h',
950+
'<Plug>(LeanInfoviewPrevHypothesis)',
951+
{ remap = true, desc = 'Move to the previous hypothesis.' }
952+
)
929953

930954
pin_buffer.keymaps:set('n', '<Plug>(LeanInfoviewGoToSuggestion)', function()
931955
iv:move_cursor_to_suggestion()
@@ -940,42 +964,78 @@ function Info:new(opts)
940964
iv:__goto('prev', is_suggestion)
941965
end, { desc = 'Move to the previous suggestion.' })
942966

943-
pin_buffer.keymaps:set('n', '<LocalLeader>S', '<Plug>(LeanInfoviewGoToSuggestion)',
944-
{ remap = true, desc = 'Move to the first suggestion.' })
945-
pin_buffer.keymaps:set('n', '<LocalLeader>s', '<Plug>(LeanInfoviewAcceptSuggestion)',
946-
{ remap = true, desc = 'Accept the first suggestion.' })
947-
pin_buffer.keymaps:set('n', ']s', '<Plug>(LeanInfoviewNextSuggestion)',
948-
{ remap = true, desc = 'Move to the next suggestion.' })
949-
pin_buffer.keymaps:set('n', '[s', '<Plug>(LeanInfoviewPrevSuggestion)',
950-
{ remap = true, desc = 'Move to the previous suggestion.' })
967+
pin_buffer.keymaps:set(
968+
'n',
969+
'<LocalLeader>S',
970+
'<Plug>(LeanInfoviewGoToSuggestion)',
971+
{ remap = true, desc = 'Move to the first suggestion.' }
972+
)
973+
pin_buffer.keymaps:set(
974+
'n',
975+
'<LocalLeader>s',
976+
'<Plug>(LeanInfoviewAcceptSuggestion)',
977+
{ remap = true, desc = 'Accept the first suggestion.' }
978+
)
979+
pin_buffer.keymaps:set(
980+
'n',
981+
']s',
982+
'<Plug>(LeanInfoviewNextSuggestion)',
983+
{ remap = true, desc = 'Move to the next suggestion.' }
984+
)
985+
pin_buffer.keymaps:set(
986+
'n',
987+
'[s',
988+
'<Plug>(LeanInfoviewPrevSuggestion)',
989+
{ remap = true, desc = 'Move to the previous suggestion.' }
990+
)
951991

952992
pin_buffer.keymaps:set('n', '<Plug>(LeanInfoviewNextLink)', function()
953993
iv:__goto('next', is_link)
954994
end, { desc = 'Move to the next link.' })
955995
pin_buffer.keymaps:set('n', '<Plug>(LeanInfoviewPrevLink)', function()
956996
iv:__goto('prev', is_link)
957997
end, { desc = 'Move to the previous link.' })
958-
pin_buffer.keymaps:set('n', ']l', '<Plug>(LeanInfoviewNextLink)',
959-
{ remap = true, desc = 'Move to the next link.' })
960-
pin_buffer.keymaps:set('n', '[l', '<Plug>(LeanInfoviewPrevLink)',
961-
{ remap = true, desc = 'Move to the previous link.' })
998+
pin_buffer.keymaps:set(
999+
'n',
1000+
']l',
1001+
'<Plug>(LeanInfoviewNextLink)',
1002+
{ remap = true, desc = 'Move to the next link.' }
1003+
)
1004+
pin_buffer.keymaps:set(
1005+
'n',
1006+
'[l',
1007+
'<Plug>(LeanInfoviewPrevLink)',
1008+
{ remap = true, desc = 'Move to the previous link.' }
1009+
)
9621010

9631011
pin_buffer.keymaps:set('n', '<Plug>(LeanInfoviewTraceSearch)', function()
9641012
iv:trace_search()
9651013
end, { desc = 'Search through trace messages in the diagnostic under the cursor.' })
966-
pin_buffer.keymaps:set('n', '<LocalLeader>/', '<Plug>(LeanInfoviewTraceSearch)',
967-
{ remap = true, desc = 'Search through trace messages in the diagnostic under the cursor.' })
1014+
pin_buffer.keymaps:set(
1015+
'n',
1016+
'<LocalLeader>/',
1017+
'<Plug>(LeanInfoviewTraceSearch)',
1018+
{ remap = true, desc = 'Search through trace messages in the diagnostic under the cursor.' }
1019+
)
9681020

9691021
pin_buffer.keymaps:set('n', '<Plug>(LeanInfoviewNextTraceDiagnostic)', function()
9701022
iv:__goto('next', is_trace_diagnostic)
9711023
end, { desc = 'Move to the next trace diagnostic.' })
9721024
pin_buffer.keymaps:set('n', '<Plug>(LeanInfoviewPrevTraceDiagnostic)', function()
9731025
iv:__goto('prev', is_trace_diagnostic)
9741026
end, { desc = 'Move to the previous trace diagnostic.' })
975-
pin_buffer.keymaps:set('n', ']t', '<Plug>(LeanInfoviewNextTraceDiagnostic)',
976-
{ remap = true, desc = 'Move to the next trace diagnostic.' })
977-
pin_buffer.keymaps:set('n', '[t', '<Plug>(LeanInfoviewPrevTraceDiagnostic)',
978-
{ remap = true, desc = 'Move to the previous trace diagnostic.' })
1027+
pin_buffer.keymaps:set(
1028+
'n',
1029+
']t',
1030+
'<Plug>(LeanInfoviewNextTraceDiagnostic)',
1031+
{ remap = true, desc = 'Move to the next trace diagnostic.' }
1032+
)
1033+
pin_buffer.keymaps:set(
1034+
'n',
1035+
'[t',
1036+
'<Plug>(LeanInfoviewPrevTraceDiagnostic)',
1037+
{ remap = true, desc = 'Move to the previous trace diagnostic.' }
1038+
)
9791039

9801040
-- Show/hide current pin extmark when entering/leaving infoview.
9811041
local pin_augroup = vim.api.nvim_create_augroup('LeanInfoviewShowPin', { clear = false })

‎lua/lean/widget/interactive_code.lua‎

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -188,14 +188,17 @@ InteractiveCode = TaggedText('SubexprInfo', render_subexpr_info)
188188
---Render a HighlightedCodeWithInfos, i.e. code where some subexpressions
189189
---may be tagged with 'highlighted' to indicate trace search matches.
190190
local HighlightedInteractiveCode
191-
HighlightedInteractiveCode = TaggedText('HighlightedSubexprInfo', function(info, tag, sess, locations)
192-
if info == 'highlighted' then
193-
local child = HighlightedInteractiveCode(tag, sess, locations)
194-
child.hlgroups = { 'leanInfoHighlighted' }
195-
return child
191+
HighlightedInteractiveCode = TaggedText(
192+
'HighlightedSubexprInfo',
193+
function(info, tag, sess, locations)
194+
if info == 'highlighted' then
195+
local child = HighlightedInteractiveCode(tag, sess, locations)
196+
child.hlgroups = { 'leanInfoHighlighted' }
197+
return child
198+
end
199+
return render_subexpr_info(info, tag, sess, locations, HighlightedInteractiveCode)
196200
end
197-
return render_subexpr_info(info, tag, sess, locations, HighlightedInteractiveCode)
198-
end)
201+
)
199202

200203
-- Exposed as a property to avoid changing the module return value.
201204
InteractiveCode.Highlighted = HighlightedInteractiveCode

‎lua/lean/widget/interactive_diagnostic.lua‎

Lines changed: 33 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -175,33 +175,41 @@ end)
175175
---Like TaggedTextMsgEmbed but additionally handles:
176176
--- - the 'highlighted' tag variant (renders children with leanInfoHighlighted)
177177
--- - expr embeds containing HighlightedCodeWithInfos
178-
interactive_diagnostic.TaggedTextHighlightedMsgEmbed = TaggedText('HighlightedMsgEmbed', function(embed, tag, sess, parent_cls)
179-
if embed == 'highlighted' then
180-
local child = interactive_diagnostic.TaggedTextHighlightedMsgEmbed(tag, sess, parent_cls)
181-
child.hlgroups = { 'leanInfoHighlighted' }
182-
return child
183-
end
184-
185-
if embed.expr then
186-
return InteractiveCode.Highlighted(embed.expr, sess)
187-
elseif embed.goal then
188-
return InteractiveGoal(embed.goal, sess)
189-
elseif embed.widget then
190-
local widget = widgets.render(embed.widget.wi, sess)
191-
if widget then
192-
return widget
178+
interactive_diagnostic.TaggedTextHighlightedMsgEmbed = TaggedText(
179+
'HighlightedMsgEmbed',
180+
function(embed, tag, sess, parent_cls)
181+
if embed == 'highlighted' then
182+
local child = interactive_diagnostic.TaggedTextHighlightedMsgEmbed(tag, sess, parent_cls)
183+
child.hlgroups = { 'leanInfoHighlighted' }
184+
return child
193185
end
194186

195-
log:debug {
196-
message = 'Widget rendering failed, falling back to the `alt` widget.',
197-
widget = embed,
198-
}
199-
return interactive_diagnostic.TaggedTextHighlightedMsgEmbed(embed.widget.alt, sess)
200-
elseif embed.trace then
201-
return render_trace(embed.trace, sess, parent_cls, interactive_diagnostic.TaggedTextHighlightedMsgEmbed)
202-
else
203-
return Element:new { text = 'malformed HighlightedMsgEmbed: ' .. vim.inspect(embed) }
187+
if embed.expr then
188+
return InteractiveCode.Highlighted(embed.expr, sess)
189+
elseif embed.goal then
190+
return InteractiveGoal(embed.goal, sess)
191+
elseif embed.widget then
192+
local widget = widgets.render(embed.widget.wi, sess)
193+
if widget then
194+
return widget
195+
end
196+
197+
log:debug {
198+
message = 'Widget rendering failed, falling back to the `alt` widget.',
199+
widget = embed,
200+
}
201+
return interactive_diagnostic.TaggedTextHighlightedMsgEmbed(embed.widget.alt, sess)
202+
elseif embed.trace then
203+
return render_trace(
204+
embed.trace,
205+
sess,
206+
parent_cls,
207+
interactive_diagnostic.TaggedTextHighlightedMsgEmbed
208+
)
209+
else
210+
return Element:new { text = 'malformed HighlightedMsgEmbed: ' .. vim.inspect(embed) }
211+
end
204212
end
205-
end)
213+
)
206214

207215
return interactive_diagnostic

‎spec/infoview/move_cursor_to_goal_spec.lua‎

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -75,10 +75,7 @@ describe(
7575
local current_infoview = infoview.get_current_infoview()
7676
helpers.wait_for_loading_pins(current_infoview)
7777

78-
assert.has_all(
79-
table.concat(current_infoview:get_lines(), '\n'),
80-
{ '| 1 = 1' }
81-
)
78+
assert.has_all(table.concat(current_infoview:get_lines(), '\n'), { '| 1 = 1' })
8279

8380
current_infoview:move_cursor_to_goal(1)
8481

@@ -89,5 +86,3 @@ describe(
8986
end
9087
)
9188
)
92-
93-

‎spec/trace_search_spec.lua‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -76,9 +76,9 @@ describe('trace search', function()
7676

7777
vim.cmd.normal { 'gg0', bang = true }
7878
vim.cmd.normal { 'n', bang = true }
79-
assert.message('n should land on a line containing the search term').is_truthy(
80-
vim.api.nvim_get_current_line():find 'Nat'
81-
)
79+
assert
80+
.message('n should land on a line containing the search term')
81+
.is_truthy(vim.api.nvim_get_current_line():find 'Nat')
8282
end
8383
)
8484
)
@@ -107,7 +107,7 @@ describe('trace search', function()
107107
vim.wait(10000, has_highlighted_extmarks)
108108

109109
-- Move the cursor in the source buffer to trigger a pin update.
110-
helpers.feed('<Plug>(LeanInfoviewGotoLastWindow)')
110+
helpers.feed '<Plug>(LeanInfoviewGotoLastWindow)'
111111
helpers.search 'rfl'
112112
helpers.wait_for_loading_pins()
113113

‎spec/tui/core_spec.lua‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -871,7 +871,11 @@ describe('BufRenderer', function()
871871
name = 'root',
872872
children = {
873873
Element:new { text = 'normal ' },
874-
Element:new { text = 'clickable', highlightable = true, events = { click = function() end } },
874+
Element:new {
875+
text = 'clickable',
876+
highlightable = true,
877+
events = { click = function() end },
878+
},
875879
},
876880
}
877881
local renderer = element:renderer { buffer = buffer }

0 commit comments

Comments
 (0)