WIP

lua/lean/infoview.lua

@@ -10,6 +10,7 @@ local infoview = {
   -- mapping from infoview IDs to infoviews
   ---@type table<number, Infoview>
   _by_tabpage = {},
+
   --- Whether to print additional debug information in the infoview.
   ---@type boolean
   debug = false,
@@ -27,6 +28,13 @@ local options = {
   show_no_info_message = false,
   use_widgets = true,
 
+  --- A filter to apply to all goal hypotheses.
+  ---@type fun(hyp: InteractiveHypothesisBundle): boolean
+  filter_hypothesis = function(k)
+    vim.print(k)
+    return true
+  end,
+
   mappings = {
     ['K'] = 'click',
     ['<CR>'] = 'click',

lua/lean/infoview/components.lua

@@ -214,20 +214,19 @@ end
 ---@param goal InteractiveGoal | InteractiveTermGoal
 ---@param sess Subsession
 local function interactive_goal(goal, sess)
-  local element = Element:new { name = 'interactive-goal' }
+  local children = {}
 
   if goal.userName ~= nil then
-    element:add_child(Element:new { text = string.format('case %s\n', goal.userName) })
+    local case = Element:new{ text = string.format('case %s\n', goal.userName) }
+    table.insert(children, case)
   end
 
-  for _, hyp in ipairs(goal.hyps) do
+  vim.iter(goal.hyps):filter(filter_hypothesis):each(function(hyp)
     local hyp_element = Element:new {
       text = table.concat(hyp.names, ' ') .. ' : ',
       name = 'hyp',
       children = { code_with_infos(hyp.type, sess) },
     }
-    element:add_child(hyp_element)
-
     if hyp.val ~= nil then
       hyp_element:add_child(Element:new {
         text = ' := ',
@@ -236,14 +235,15 @@ local function interactive_goal(goal, sess)
       })
     end
     hyp_element:add_child(Element:new { text = '\n', name = 'hypothesis-separator' })
-  end
+    table.insert(children, hyp_element)
+  end)
 
-  element:add_child(Element:new {
+  table.insert(children, Element:new {
     text = '⊢ ',
     name = 'goal',
     children = { code_with_infos(goal.type, sess) },
   })
-  return element
+  return Element:new{ name = 'interactive-goal', children = children }
 end
 
 ---@param goal InteractiveGoals?