Implement highlighting for goal state diffing.

This adds support for two of the three kinds Lean sends:

    * showing when terms are changing
      (implementation-wise, this is from `SubexprInfo`)
    * showing when hypotheses are changing
      (implementation-wise, this is from `InteractiveHypothesisBundle`)

There's a third type we don't add support for which Lean sends (in
`InteractiveGoal`) which indicates whether whole goals are changing, and
in VSCode this is indicated via some indent-guide-like lines that appear
to the left of the goal.

We're choosing to skip that for now since it'd mean adding some sort of
similar indent-guide-y highlights. Let's wait to see if users want it
first, even though doing so should be possible by looking at however an
indent-guide plugin does it.

doc/tags

@@ -7,6 +7,8 @@ Lean.SatelliteConfig	lean.txt	/*Lean.SatelliteConfig*
 LeanFileProgressParams	lean.txt	/*LeanFileProgressParams*
 LoogleResult	lean.txt	/*LoogleResult*
 Pin	lean.txt	/*Pin*
+PlainGoal	lean.txt	/*PlainGoal*
+PlainTermGoal	lean.txt	/*PlainTermGoal*
 abbreviations.convert	lean.txt	/*abbreviations.convert*
 abbreviations.enable	lean.txt	/*abbreviations.enable*
 abbreviations.load	lean.txt	/*abbreviations.load*

lua/lean/infoview/components.lua

@@ -7,6 +7,7 @@
 
 local Element = require('lean.tui').Element
 local config = require 'lean.config'
+local log = require 'lean.log'
 local rpc = require 'lean.rpc'
 local util = require 'lean._util'
 local widgets = require 'lean.widgets'
@@ -16,6 +17,19 @@ local components = {
   PROCESSING = Element:new { text = 'Processing file...', name = 'processing' },
 }
 
+---A user-facing explanation of a changing piece of the goal state.
+---
+---Corresponds to equivalent VSCode explanations.
+---@type table<DiffTag, string>
+local DIFF_TAG_TO_EXPLANATION = {
+  wasChanged = 'This subexpression has been modified.',
+  willChange = 'This subexpression will be modified.',
+  wasInserted = 'This subexpression has been inserted.',
+  willInsert = 'This subexpression will be inserted.',
+  wasDeleted = 'This subexpression has been removed.',
+  willDelete = 'This subexpression will be deleted.',
+}
+
 ---Format a heading.
 local function H(contents)
   return ('▶ %s'):format(contents)
@@ -112,6 +126,17 @@ local function code_with_infos(t, sess)
 
     local info_open = false
 
+    if subexpr_info.diffStatus then
+      if element.hlgroup then
+        log:warning {
+          message = 'quashing a highlight group',
+          hlgroup = element.hlgroup,
+          diffStatus = subexpr_info.diffStatus,
+        }
+      end
+      element.hlgroup = 'leanInfoDiff' .. subexpr_info.diffStatus
+    end
+
     local do_reset = function(ctx)
       info_open = false
       element:remove_tooltip()
@@ -125,7 +150,7 @@ local function code_with_infos(t, sess)
       if info_popup.exprExplicit ~= nil then
         tooltip_element:add_child(code_with_infos(info_popup.exprExplicit, sess))
         if info_popup.type ~= nil then
-          tooltip_element:add_child(Element:new { text = ' :\n' })
+          tooltip_element:add_child(Element:new { text = ' : ' })
         end
       end
 
@@ -138,6 +163,14 @@ local function code_with_infos(t, sess)
         tooltip_element:add_child(Element:new { text = info_popup.doc }) -- TODO: markdown
       end
 
+      if subexpr_info.diffStatus then
+        tooltip_element:add_child(Element:new { text = '\n\n' })
+        tooltip_element:add_child(Element:new {
+          hlgroup = 'Comment',
+          text = DIFF_TAG_TO_EXPLANATION[subexpr_info.diffStatus],
+        })
+      end
+
       return tooltip_element
     end
 
@@ -245,9 +278,17 @@ local function to_hypotheses_element(hyps, opts, sess)
     end
 
     local element = Element:new {
-      text = names:join ' ' .. ' : ',
       name = 'hyp',
-      children = { code_with_infos(hyp.type, sess) },
+      children = {
+        Element:new {
+          text = names:join ' ',
+          hlgroup = hyp.isInserted and 'leanInfoHypNameInserted'
+            or hyp.isRemoved and 'leanInfoHypNameRemoved'
+            or nil,
+        },
+        Element:new { text = ' : ' },
+        code_with_infos(hyp.type, sess),
+      },
     }
 
     if opts.show_let_values and hyp.val then

spec/infoview/tooltips_spec.lua

@@ -34,7 +34,7 @@ describe(
       helpers.feed '<CR>'
       local tooltip_bufnr = vim.api.nvim_win_get_buf(helpers.wait_for_new_window(known_windows))
       assert.contents.are {
-        'Type :\nType 1\n\nA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ',
+        'Type : Type 1\n\nA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. ',
         bufnr = tooltip_bufnr,
       }
 

syntax/leaninfo.lua

@@ -29,7 +29,7 @@ highlight [[default link leanInfoExpectedType Special]]
 -- Diagnostics
 
 ---@type table<lsp.Diagnostic, string>
-local HLGROUPS = {
+local DIAGNOSTIC_HLGROUPS = {
   'DiagnosticError',
   'DiagnosticWarn',
   'DiagnosticInfo',
@@ -38,7 +38,7 @@ local HLGROUPS = {
 
 ---@type string, string
 local match, hlgroup
-for i, to_group in vim.iter(ipairs(HLGROUPS)) do
+for i, to_group in vim.iter(ipairs(DIAGNOSTIC_HLGROUPS)) do
   match = config.severity_markers[i]:gsub('\n', [[\_$]])
   hlgroup = 'leanInfo' .. to_group
   syntax(('match %s "^▶.*: %s.*$"'):format(hlgroup, match))
@@ -48,6 +48,24 @@ end
 syntax [[match leanInfoComment "--.*"]]
 highlight [[default link leanInfoComment Comment]]
 
+-- Goal Diffing
+
+highlight [[default link leanInfoHypNameInserted DiffAdd]]
+highlight [[default link leanInfoHypNameRemoved DiffDelete]]
+
+---@type table<DiffTag, string>
+local DIFF_TAG_HLGROUPS = {
+  wasChanged = 'DiffText',
+  willChange = 'DiffDelete',
+  wasInserted = 'DiffAdd',
+  willInsert = 'DiffAdd',
+  wasDeleted = 'DiffDelete',
+  willDelete = 'DiffDelete',
+}
+for diff_tag, to_group in vim.iter(DIFF_TAG_HLGROUPS) do
+  highlight(('default link leanInfoDiff%s %s'):format(diff_tag, to_group))
+end
+
 -- Widgets
 
 syntax [[match widgetSuggestions "^▶ suggestions.*"]]