fix: have the delaborator tag functions being applied

leanprover · Feb 12, 2024 · 20d75c1 · 20d75c1
1 parent a92401a
commit 20d75c1
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/src/verso-blog/Verso/Genre/Blog/HighlightCode.lean b/src/verso-blog/Verso/Genre/Blog/HighlightCode.lean
@@ -494,7 +494,11 @@ def findTactics (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : Syntax) : Highl
           let name := if mvDecl.userName.isAnonymous then none else some mvDecl.userName
           let lctx := mvDecl.lctx |>.sanitizeNames.run' {options := (← getOptions)}
 
-          let runMeta {α} (act : MetaM α) : HighlightM α := ci.runMetaM lctx act
+          -- Tell the delaborator to tag functions that are being applied. Otherwise,
+          -- functions have no tooltips or binding info in tactics.
+          -- cf https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Function.20application.20delaboration/near/265800665
+          let ci' := {ci with options := ci.options.set `pp.tagAppFns true}
+          let runMeta {α} (act : MetaM α) : HighlightM α := ci'.runMetaM lctx act
           for c in lctx.decls do
             let some decl := c
               | continue