From 3d175ab25fb0f548be3b5d29f376ed8e32f10137 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 14 Oct 2024 10:28:28 -0700 Subject: [PATCH] =?UTF-8?q?fix:=20the=20`=E2=8B=AF`=20elaboration=20warnin?= =?UTF-8?q?g=20did=20not=20mention=20`pp.maxSteps`=20(#5710)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This also adds in the tip that hovering over `⋯` gives the option that led to its presence. --- src/Lean/Elab/BuiltinTerm.lean | 8 +++++--- tests/lean/ppDeepTerms.lean.expected.out | 4 ++-- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean index 38fd868b00..f9a225b9b6 100644 --- a/src/Lean/Elab/BuiltinTerm.lean +++ b/src/Lean/Elab/BuiltinTerm.lean @@ -103,9 +103,11 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level := @[builtin_term_elab Lean.Parser.Term.omission] def elabOmission : TermElab := fun stx expectedType? => do logWarning m!"\ 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 `_`.\ - \n\nThe 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`." + It logs this warning and then elaborates like '_'.\ + \n\n\ + The presence of '⋯' in pretty printing output is controlled by the 'pp.maxSteps', 'pp.deepTerms' and 'pp.proofs' options. \ + These options can be further adjusted using 'pp.deepTerms.threshold' and 'pp.proofs.threshold'. \ + If this '⋯' was copied from the Infoview, the hover there for the original '⋯' explains which of these options led to the omission." elabHole stx expectedType? @[builtin_term_elab «letMVar»] def elabLetMVar : TermElab := fun stx expectedType? => do diff --git a/tests/lean/ppDeepTerms.lean.expected.out b/tests/lean/ppDeepTerms.lean.expected.out index 3bc3c796bf..8b86c94c57 100644 --- a/tests/lean/ppDeepTerms.lean.expected.out +++ b/tests/lean/ppDeepTerms.lean.expected.out @@ -3,7 +3,7 @@ Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ : Nat ⋯.succ.succ.succ.succ.succ.succ.succ.succ.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 `_`. +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`. +The presence of '⋯' in pretty printing output is controlled by the 'pp.maxSteps', 'pp.deepTerms' and 'pp.proofs' options. These options can be further adjusted using 'pp.deepTerms.threshold' and 'pp.proofs.threshold'. If this '⋯' was copied from the Infoview, the hover there for the original '⋯' explains which of these options led to the omission. [1, 2, 3, 4, 5, 6, 7, 8, ?m] : List Nat