From 90f92c3a9e18767f3ff57786b81ce7247ef3f11e Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Wed, 24 Aug 2022 14:55:43 +0200
Subject: [PATCH] fix: use delabAppExplicit for tooltips

---
 src/Lean/PrettyPrinter.lean          |  4 ++--
 src/Lean/Widget/InteractiveCode.lean | 16 ++++++++--------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index 531c6f0f1d..0ecf9dc1d9 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -37,11 +37,11 @@ def ppExpr (e : Expr) : MetaM Format := do
 
 /-- Return a `fmt` representing pretty-printed `e` together with a map from tags in `fmt`
 to `Elab.Info` nodes produced by the delaborator at various subexpressions of `e`. -/
-def ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := {})
+def ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := {}) (delab := Delaborator.delab)
     : MetaM (Format × Std.RBMap Nat Elab.Info compare) := do
   let lctx := (← getLCtx).sanitizeNames.run' { options := (← getOptions) }
   Meta.withLCtx lctx #[] do
-    let (stx, infos) ← delabCore e optsPerPos
+    let (stx, infos) ← delabCore e optsPerPos delab
     let fmt ← ppTerm stx
     return (fmt, infos)
 
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index 6258bc7c3f..9529107253 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -44,14 +44,14 @@ where
       | some i => TaggedText.tag ⟨WithRpcRef.mk { ctx, info := i }, n⟩ (go subTt)
 
 def ppExprTagged (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := do
-  let optsPerPos := if explicit then
-    Std.RBMap.ofList [
-      (SubExpr.Pos.root, KVMap.empty.setBool `pp.all true),
-      (SubExpr.Pos.root, KVMap.empty.setBool `pp.tagAppFns true)
-    ]
-  else
-    {}
-  let (fmt, infos) ← PrettyPrinter.ppExprWithInfos e optsPerPos
+  let delab := open PrettyPrinter.Delaborator in
+    if explicit then
+      withOptionAtCurrPos pp.tagAppFns.name true do
+      withOptionAtCurrPos pp.explicit.name true do
+        delabAppImplicit <|> delabAppExplicit
+    else
+      delab
+  let (fmt, infos) ← PrettyPrinter.ppExprWithInfos e (delab := delab)
   let tt := TaggedText.prettyTagged fmt
   let ctx := {
     env           := (← getEnv)