From 11e10459bbb786294f56570969e554c96fdcd3bd Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Sun, 24 Apr 2022 19:24:28 -0400
Subject: [PATCH] refactor: move function to PrettyPrinter

---
 src/Lean/PrettyPrinter.lean                | 10 ++++++++
 src/Lean/Widget/InteractiveCode.lean       | 29 +++++-----------------
 src/Lean/Widget/InteractiveDiagnostic.lean |  5 ++--
 3 files changed, 19 insertions(+), 25 deletions(-)

diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean
index d7581bdaa6..00afedfeda 100644
--- a/src/Lean/PrettyPrinter.lean
+++ b/src/Lean/PrettyPrinter.lean
@@ -33,6 +33,16 @@ def ppUsing (e : Expr) (delab : Expr → MetaM Syntax) : MetaM Format := do
 def ppExpr (e : Expr) : MetaM Format := do
   ppUsing e delab
 
+/-- 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 := {})
+    : 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 fmt ← ppTerm stx
+    return (fmt, infos)
+
 def ppConst (e : Expr) : MetaM Format := do
   ppUsing e fun e => return (← delabCore e (delab := Delaborator.delabConst)).1
 
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index c640ce1a81..15c90325bd 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Wojciech Nawrocki
 -/
-import Lean.PrettyPrinter.Delaborator.Basic
+import Lean.PrettyPrinter
 import Lean.Server.Rpc.Basic
 import Lean.Widget.TaggedText
 
@@ -71,27 +71,6 @@ where
         | 0, proj _ _ e₁ _ => go' e₁
         | _, _             => return (lctx, e) -- panic! s!"cannot descend {a} into {e.expr}"
 
--- TODO(WN): should the two fns below go in `Lean.PrettyPrinter` ?
-open PrettyPrinter in
-private def formatWithOpts (e : Expr) (optsPerPos : Delaborator.OptionsPerPos)
-    : MetaM (Format × Std.RBMap Nat Elab.Info compare) := do
-    let opts ← getOptions
-    let e ← Meta.instantiateMVars e
-    let (stx, infos) ← PrettyPrinter.delabCore e optsPerPos
-    let stx := sanitizeSyntax stx |>.run' { options := opts }
-    let stx ← PrettyPrinter.parenthesizeTerm stx
-    let fmt ← PrettyPrinter.formatTerm stx
-    return (fmt, infos)
-
-/-- Pretty-print the expression and its subexpression information. When `explicit := true`,
-we set `pp.all` at the top-level expression. -/
-def formatInfos (e : Expr) (explicit : Bool) : MetaM (Format × Std.RBMap Nat Elab.Info compare) :=
-  let optsPerPos := if explicit then
-    Std.RBMap.ofList [(1, KVMap.empty.setBool `pp.all true)]
-  else
-    {}
-  formatWithOpts e optsPerPos
-
 /-- Tags a pretty-printed `Expr` with infos from the delaborator. -/
 partial def tagExprInfos (ctx : Elab.ContextInfo) (infos : Std.RBMap Nat Elab.Info compare) (tt : TaggedText (Nat × Nat))
     : CodeWithInfos :=
@@ -104,7 +83,11 @@ where
       | some i => TaggedText.tag ⟨WithRpcRef.mk { ctx, info := i }⟩ (go subTt)
 
 def exprToInteractive (e : Expr) (explicit : Bool := false) : MetaM CodeWithInfos := do
-  let (fmt, infos) ← formatInfos e explicit
+  let optsPerPos := if explicit then
+    Std.RBMap.ofList [(1, KVMap.empty.setBool `pp.all true)]
+  else
+    {}
+  let (fmt, infos) ← PrettyPrinter.ppExprWithInfos e optsPerPos
   let tt := TaggedText.prettyTagged fmt
   let ctx := {
     env           := (← getEnv)
diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean
index 828ce19e25..64b4719c77 100644
--- a/src/Lean/Widget/InteractiveDiagnostic.lean
+++ b/src/Lean/Widget/InteractiveDiagnostic.lean
@@ -129,9 +129,10 @@ where
       options       := ctx.opts
       currNamespace := nCtx.currNamespace
       openDecls     := nCtx.openDecls
-      ngen          := { namePrefix := `_diag } -- Hack: to make sure unique ids created at `formatInfos` do not collide with ones in `ctx.mctx`
+      -- Hack: to make sure unique ids created at `ppExprWithInfos` do not collide with ones in `ctx.mctx`
+      ngen          := { namePrefix := `_diag }
     }
-    let (fmt, infos) ← ci.runMetaM ctx.lctx <| formatInfos e (explicit := false)
+    let (fmt, infos) ← ci.runMetaM ctx.lctx <| PrettyPrinter.ppExprWithInfos e
     let t ← pushEmbed <| EmbedFmt.expr ci infos
     return Format.tag t fmt
   | _,    none,      ofGoal mvarId            => pure $ "goal " ++ format (mkMVar mvarId)