fix: use delabAppExplicit for tooltips

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)
 

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)