max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: the ⋯ elaboration warning did not mention pp.maxSteps (#5710)

Browse source 
This also adds in the tip that hovering over `⋯` gives the option that
led to its presence.
This commit is contained in:
Kyle Miller 2024-10-14 10:28:28 -07:00 • committed by GitHub
parent 9b6696be1d
commit 3d175ab25f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Elab/BuiltinTerm.lean
View file

@ -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

4
tests/lean/ppDeepTerms.lean.expected.out
View file

@ -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