From 859dbb71779e254754e3d73b8ac57710bebe8a62 Mon Sep 17 00:00:00 2001 From: Julian Berman Date: Wed, 9 Oct 2024 20:28:50 -0400 Subject: [PATCH] Syntax highlight GoToModuleLinks. --- lua/lean/widgets.lua | 2 ++ syntax/leaninfo.vim | 2 ++ 2 files changed, 4 insertions(+) diff --git a/lua/lean/widgets.lua b/lua/lean/widgets.lua index dc95a58e..7847d805 100644 --- a/lua/lean/widgets.lua +++ b/lua/lean/widgets.lua @@ -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() diff --git a/syntax/leaninfo.vim b/syntax/leaninfo.vim index 0e867549..9ffe0ad5 100644 --- a/syntax/leaninfo.vim +++ b/syntax/leaninfo.vim @@ -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