diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean
index c322bd3108..e728e723fc 100644
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -181,7 +181,7 @@ syntax (name := calcTactic) "calc" calcSteps : tactic
     match tail with
     | `([])      => `([$x])
     | `([$xs,*]) => `([$x, $xs,*])
-    --| `(⋯)       => `([$x, $tail]) -- Unexpands to `[x, y, z, ⋯]` for `⋯ : List α`
+    | `(⋯)       => `([$x, $tail]) -- Unexpands to `[x, y, z, ⋯]` for `⋯ : List α`
     | _          => throw ()
   | _ => throw ()
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
index e636ec808c..3e1138d77a 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean
@@ -328,8 +328,7 @@ Delaborates the current expression as `⋯` and attaches `Elab.OmissionInfo`, wh
 subterm omitted by `⋯` is delaborated when hovered over.
 -/
 def omission : Delab := do
-  --let stx ← `(⋯)
-  let stx : Term := ⟨mkNode ``Lean.Parser.Term.omission #[]⟩
+  let stx ← `(⋯)
   let stx ← annotateCurPos stx
   addOmissionInfo (← getPos) stx (← getExpr)
   pure stx
diff --git a/tests/lean/run/deepTerms.lean b/tests/lean/ppDeepTerms.lean
similarity index 87%
rename from tests/lean/run/deepTerms.lean
rename to tests/lean/ppDeepTerms.lean
index 0d0fa1d76d..8afd17f864 100644
--- a/tests/lean/run/deepTerms.lean
+++ b/tests/lean/ppDeepTerms.lean
@@ -32,3 +32,8 @@ Nothing is omitted in short lists
 In longer lists, the tail is omitted
 -/
 #check [1, 2, 3, 4, 5, 6, 7, 8, 9]
+
+/-!
+Checking the message when an omission is copied from the Infoview
+-/
+#check [1, 2, 3, 4, 5, 6, 7, 8, ⋯]
diff --git a/tests/lean/ppDeepTerms.lean.expected.out b/tests/lean/ppDeepTerms.lean.expected.out
new file mode 100644
index 0000000000..a4072a7378
--- /dev/null
+++ b/tests/lean/ppDeepTerms.lean.expected.out
@@ -0,0 +1,10 @@
+Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))))) : Nat
+Nat.succ
+  (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))))))) : Nat
+Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ ⋯)))))))) : Nat
+[1, 2, 3, 4, 5, 6, 7, 8] : List Nat
+[1, 2, 3, 4, 5, 6, 7, 8, ⋯] : List Nat
+ppDeepTerms.lean:39:32-39:33: warning: The '⋯' token is used by the pretty printer to indicate omitted terms, and it should not be used directly. It logs this warning and then elaborates like `_`.
+
+The presence of `⋯` in pretty printing output is controlled by the 'pp.deepTerms' and `pp.proofs` options. These options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`.
+[1, 2, 3, 4, 5, 6, 7, 8, ?m] : List Nat
diff --git a/tests/lean/run/deepTerms.lean.expected.out b/tests/lean/run/deepTerms.lean.expected.out
deleted file mode 100644
index c3c4204351..0000000000
--- a/tests/lean/run/deepTerms.lean.expected.out
+++ /dev/null
@@ -1,6 +0,0 @@
-Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))))) : Nat
-Nat.succ
-  (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))))))) : Nat
-Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ ⋯)))))))) : Nat
-[1, 2, 3, 4, 5, 6, 7, 8] : List Nat
-[1, 2, 3, 4, 5, 6, 7, 8, ⋯] : List Nat