tui: support multiple hlgroups per Element

Element.hlgroup (now hlgroups) accepted only a single string or a
function returning one, making it impossible to apply two orthogonal
highlights to the same element. In particular, interactive_code's
diff-status highlight was silently dropped whenever the element was
also selectable, because the locations function assignment overwrote
the diff string.

hlgroups is now always a string[] (or a function returning one).
interactive_code returns both groups when an element has a diff status
and is simultaneously selected.

Author: Julian

lua/lean/infoview/components.lua

@@ -22,7 +22,7 @@ local widgets = require 'lean.widgets'
 local components = {
   LSP_HAS_DIED = Element:new {
     text = '🪦 The Lean language server is dead.',
-    hlgroup = 'DiagnosticError',
+    hlgroups = { 'DiagnosticError' },
   },
   NO_INFO = Element:new { text = 'No info.', name = 'no-info' },
   PROCESSING = Element:new { text = 'Processing file...', name = 'processing' },

lua/lean/infoview/locations.lua

@@ -176,7 +176,7 @@ function Locations:toggle_subexpr_selection(pos)
   self:toggle_selection(self:template_with_subexpr_pos(pos))
 end
 
---TODO: have Locations handle constructing hlgroup()
+--TODO: have Locations handle constructing hlgroups()
 ---@param pos SubexprPos
 function Locations:is_subexpr_selected(pos)
   return self:is_selected(self:template_with_subexpr_pos(pos))

lua/lean/tui.lua

@@ -42,7 +42,7 @@ local log = require 'lean.log'
 ---@field events EventCallbacks functions to fire for events which this element responds to
 ---@field text string the text to show when rendering this element
 ---@field name string a named handle for this element, used when path-searching
----@field hlgroup? string|fun(string):string? the highlight group for this element's text, or a function that returns it
+---@field hlgroups? string[]|fun():string[]|nil the highlight group(s) for this element's text, or a function that returns them
 ---@field tooltip? Element? tooltip
 ---@field highlightable boolean (for buffer rendering) whether to highlight this element when hovering over it
 ---@field _size? integer Computed size of this element, updated by `Element:to_string`
@@ -73,7 +73,7 @@ BufRenderer.__index = BufRenderer
 ---@field events? EventCallbacks event function map
 ---@field text? string the text to show when rendering this element
 ---@field name? string a named handle for this element, used when path-searching
----@field hlgroup? string|fun():string? the highlight group for this element's text, or a function that returns it
+---@field hlgroups? string[]|fun():string[]|nil the highlight group(s) for this element's text, or a function that returns them
 ---@field highlightable boolean? (for buffer rendering) whether to highlight this element when hovering over it
 ---@field children? Element[] this element's children
 ---@field private __async_init? fun(on_result: fun(Element):nil):nil
@@ -86,7 +86,7 @@ function Element:new(args)
   local obj = {
     text = args.text or '',
     name = args.name or '',
-    hlgroup = args.hlgroup,
+    hlgroups = args.hlgroups,
     highlightable = args.highlightable or false,
     events = args.events or {},
     __children = args.children or {},
@@ -114,7 +114,7 @@ function Element:titled(opts)
     return body
   end
 
-  local title = self:new { text = opts.title, hlgroup = opts.title_hlgroup }
+  local title = self:new { text = opts.title, hlgroups = opts.title_hlgroup and { opts.title_hlgroup } or nil }
 
   if not body then
     return title
@@ -189,7 +189,7 @@ function Element.select(choices, opts, on_choice)
       Element:new { text =  ' ▾' },
     },
     highlightable = true,
-    hlgroup = 'widgetSelect',
+    hlgroups = { 'widgetSelect' },
     events = {
       click = function(ctx)
         vim.ui.select(choices, {
@@ -214,7 +214,7 @@ end
 ---@param key string
 ---@return Element
 function Element.kbd(key)
-  return Element:new { text = key, hlgroup = 'widgetKbd' }
+  return Element:new { text = key, hlgroups = { 'widgetKbd' } }
 end
 
 ---Create an Element whose click event does nothing.
@@ -308,16 +308,18 @@ function Element:_get_highlights()
   ---@param element Element
   ---@param pos integer
   local function go(element, pos)
-    local hlgroup = element.hlgroup
-    if type(hlgroup) == 'function' then
-      hlgroup = hlgroup(element)
+    local hlgroups = element.hlgroups
+    if type(hlgroups) == 'function' then
+      hlgroups = hlgroups(element)
     end
-    if hlgroup then
-      table.insert(hls, {
-        start = pos,
-        ['end'] = pos + element._size,
-        hlgroup = hlgroup,
-      })
+    if hlgroups then
+      for _, hg in ipairs(hlgroups) do
+        table.insert(hls, {
+          start = pos,
+          ['end'] = pos + element._size,
+          hlgroup = hg,
+        })
+      end
     end
 
     pos = pos + #element.text

lua/lean/widget/interactive_code.lua

@@ -31,7 +31,7 @@ local InteractiveCode
 local function render_subexpr_info(subexpr_info, tag, sess, locations)
   local element = Element:new { highlightable = true }
   if subexpr_info.diffStatus then
-    element.hlgroup = 'leanInfoDiff' .. subexpr_info.diffStatus
+    element.hlgroups = { 'leanInfoDiff' .. subexpr_info.diffStatus }
   end
 
   local info_open = false
@@ -66,7 +66,7 @@ local function render_subexpr_info(subexpr_info, tag, sess, locations)
     if subexpr_info.diffStatus then
       tooltip_element:add_child(Element:new { text = '\n\n' })
       tooltip_element:add_child(Element:new {
-        hlgroup = 'Comment',
+        hlgroups = { 'Comment' },
         text = DIFF_TAG_TO_EXPLANATION[subexpr_info.diffStatus],
       })
     end
@@ -146,8 +146,16 @@ local function render_subexpr_info(subexpr_info, tag, sess, locations)
   }
 
   if locations then
-    function element.hlgroup()
-      return locations:is_subexpr_selected(subexpr_info.subexprPos) and 'leanInfoSelected' or nil
+    local diff_hl = element.hlgroups ---@type string[]?
+    function element.hlgroups()
+      local selected = locations:is_subexpr_selected(subexpr_info.subexprPos)
+      if diff_hl and selected then
+        return vim.iter({ diff_hl, { 'leanInfoSelected' } }):flatten():totable()
+      elseif selected then
+        return { 'leanInfoSelected' }
+      else
+        return diff_hl
+      end
     end
     element.events.select = function()
       locations:toggle_subexpr_selection(subexpr_info.subexprPos)

lua/lean/widget/interactive_goal.lua

@@ -19,21 +19,21 @@ end
 ---@param fvar_id FVarId
 ---@param locations? Locations
 local function to_hypothesis_name(name, mvar_id, fvar_id, locations)
-  local function accessible_hlgroup()
-    return is_accessible(name) and 'leanInfoHypName' or 'leanInfoInaccessibleHypName'
+  local function accessible_hlgroups()
+    return { is_accessible(name) and 'leanInfoHypName' or 'leanInfoInaccessibleHypName' }
   end
 
   local highlightable, select
-  local hlgroup = accessible_hlgroup
+  local hlgroups = accessible_hlgroups
 
   if locations and mvar_id and fvar_id then
     highlightable = true
 
     ---@type GoalsLocation
     local location = { mvarId = mvar_id, loc = { hyp = fvar_id } }
 
-    hlgroup = function()
-      return locations:is_selected(location) and 'leanInfoSelected' or accessible_hlgroup()
+    hlgroups = function()
+      return locations:is_selected(location) and { 'leanInfoSelected' } or accessible_hlgroups()
     end
 
     select = function()
@@ -44,7 +44,7 @@ local function to_hypothesis_name(name, mvar_id, fvar_id, locations)
   return Element:new {
     text = name,
     highlightable = highlightable,
-    hlgroup = hlgroup,
+    hlgroups = hlgroups,
     events = { select = select },
   }
 end
@@ -84,8 +84,8 @@ local function to_hypothesis_element(hyp, mvar_id, opts, sess, locations)
     name = 'hyp',
     children = {
       Element:concat(names, ' ', {
-        hlgroup = hyp.isInserted and 'leanInfoHypNameInserted'
-          or hyp.isRemoved and 'leanInfoHypNameRemoved'
+        hlgroups = hyp.isInserted and { 'leanInfoHypNameInserted' }
+          or hyp.isRemoved and { 'leanInfoHypNameRemoved' }
           or nil,
       }),
       Element:new { text = ' : ' },
@@ -166,7 +166,7 @@ function interactive_goal.Goal(goal, sess, locations)
   if goal.userName then
     case = Element:new {
       children = {
-        Element:new { text = 'case ', hlgroup = 'leanInfoGoalCase' },
+        Element:new { text = 'case ', hlgroups = { 'leanInfoGoalCase' } },
         Element:new { text = goal.userName .. '\n' },
       },
     }
@@ -182,7 +182,7 @@ function interactive_goal.Goal(goal, sess, locations)
   local goal_element = Element:new {
     name = 'goal',
     children = {
-      Element:new { text = goal.goalPrefix or '⊢ ', hlgroup = 'leanInfoGoalPrefix' },
+      Element:new { text = goal.goalPrefix or '⊢ ', hlgroups = { 'leanInfoGoalPrefix' } },
       InteractiveCode(goal.type, sess, goal_locations),
     },
   }

lua/lean/widgets/GoToModuleLink.lua

@@ -16,7 +16,7 @@ return function(ctx, props)
   return Element:new {
     text = props.modName,
     highlightable = true,
-    hlgroup = 'widgetLink',
+    hlgroups = { 'widgetLink' },
     events = {
       go_to_def = function(_)
         local last_window = ctx.get_last_window()

lua/lean/widgets/Lean/Meta/Hint/textInsertionWidget.lua

@@ -32,7 +32,7 @@ return function(ctx, props)
     text = props.acceptSuggestionProps.linkText,
     children = Element:new { text = props.suggestion },
     highlightable = true,
-    hlgroup = 'widgetLink',
+    hlgroups = { 'widgetLink' },
     events = {
       click = function()
         ctx:apply_edits {

lua/lean/widgets/Lean/Meta/Hint/tryThisDiffWidget.lua

@@ -28,7 +28,7 @@ return function(ctx, props)
   return Element:new {
     text = props.suggestion,
     highlightable = true,
-    hlgroup = 'widgetLink',
+    hlgroups = { 'widgetLink' },
     events = {
       click = function()
         ctx:apply_edits {

lua/lean/widgets/Lean/Meta/Tactic/TryThis/tryThisWidget.lua

@@ -26,7 +26,7 @@ return function(ctx, props)
       Element:new {
         text = each.suggestion,
         highlightable = true,
-        hlgroup = 'widgetLink',
+        hlgroups = { 'widgetLink' },
         events = {
           click = function()
             ctx:apply_edits {

lua/lean/widgets/Lean/errorDescriptionWidget.lua

@@ -13,7 +13,7 @@ return function(_, props)
       Element:new {
         text = 'View explanation',
         highlightable = true,
-        hlgroup = 'widgetLink',
+        hlgroups = { 'widgetLink' },
         events = {
           click = function()
             vim.ui.open(props.explanationUrl)