From 08e149de15843b9c2adf3890b66539ea2e720b83 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sat, 24 Feb 2024 08:59:19 -0800
Subject: [PATCH] fix: make omission syntax be a builtin syntax (part 2)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Re-enables `⋯` processing that was disabled during the move to a builtin.
Adds tests.
---
 src/Init/NotationExtra.lean                         |  2 +-
 src/Lean/PrettyPrinter/Delaborator/Basic.lean       |  3 +--
 tests/lean/{run/deepTerms.lean => ppDeepTerms.lean} |  5 +++++
 tests/lean/ppDeepTerms.lean.expected.out            | 10 ++++++++++
 tests/lean/run/deepTerms.lean.expected.out          |  6 ------
 5 files changed, 17 insertions(+), 9 deletions(-)
 rename tests/lean/{run/deepTerms.lean => ppDeepTerms.lean} (87%)
 create mode 100644 tests/lean/ppDeepTerms.lean.expected.out
 delete mode 100644 tests/lean/run/deepTerms.lean.expected.out

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