Skip to content

Commit

Permalink
Syntax highlight GoToModuleLinks.
Browse files Browse the repository at this point in the history
  • Loading branch information
Julian committed Oct 10, 2024
1 parent 8adb90d commit 859dbb7
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 0 deletions.
2 changes: 2 additions & 0 deletions lua/lean/widgets.lua
Original file line number Diff line number Diff line change
Expand Up @@ -110,6 +110,8 @@ end)
implement('GoToModuleLink', function(_, props)
return Element:new {
text = props.modName,
highlightable = true,
hlgroup = 'widgetLink',
events = {
go_to_def = function(_)
local this_infoview = require('lean.infoview').get_current_infoview()
Expand Down
2 changes: 2 additions & 0 deletions syntax/leaninfo.vim
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,8 @@ hi def link widgetElementLoading Comment
hi def link widgetSuggestions Title
hi def link widgetSuggestionsSubgoals Statement

hi def link widgetLink Tag

hi def link leanInfoExternalHighlight widgetElementHighlight
hi def link leanInfoButton Pmenu
hi def link leanInfoField Folded
Expand Down

0 comments on commit 859dbb7

Please sign in to comment.