Repository navigation
PDF: set Markdown block quotes as quotations - #228
Merged
Merged
Conversation
`Latex.prose` had no case for a block quote, so a docstring's quotation was
joined into a paragraph with its `>` marks kept, and the PDF showed them
mid-sentence. A run of `>` lines is now stripped of one `>` and an optional
space, rendered as prose in its own right (so it may hold paragraphs or a
list), and wrapped in `\begin{quote}`. A `#guard` pins the rendering.
`argtex` and `exampletex` now refuse to write or pass a document with a line,
outside verbatim, that begins with `>` (`strayQuoteLines`), so a block quote
that reaches the LaTeX unconverted fails the generator rather than the reader.
`docs/latex/arguments.tex` regenerated: all 34 quotations are now quote
environments. The site's Markdown pages are unchanged.
Closes #227.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01SkMSatapwS49wkbWE3RMEj
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No verdict moves; this changes how the PDF prints quotations. Closes #227.
What this changes
Testimony.Logic.Latex.prosehad no case for a Markdown block quote. A docstring's quotation was joined into one paragraph with its>marks kept, so the PDF showed them mid-sentence. A run of>lines is now handled like this: one>and an optional space come off each line, the text inside is rendered withproseagain (so a quote may hold several paragraphs or a list), and the result is wrapped in\begin{quote} … \end{quote}. A blank>line separates paragraphs inside the quote. A>line also ends a paragraph directly above it, as it does in Markdown.To stop this from coming back without anyone noticing,
argtexandexampletexnow refuse to write a document, or pass--check, if any line outside a verbatim block begins with>. The check isTestimony.Doc.strayQuoteLines, inTestimony/Tools/Pages.lean.docs/latex/arguments.texis regenerated. All 34 quotations the issue counted are nowquoteenvironments, and no line begins with>.What it claims, and what it does not
It claims that a block quote in any docstring now prints as an indented quotation in the PDF. It also claims that a quote reaching the LaTeX unconverted fails the generator. Both are pinned by
#guards: one onprosewith a quote holding a paragraph and a list, one onstrayQuoteLines.It does not handle a "lazy" continuation, which is a plain line straight after a
>line that Markdown would fold into the quote. No docstring in the repository has one. If one is written, the new check fails, so it cannot slip into the PDF unseen. Nested quotes (> >) work because the renderer runs again on the inner text, but no docstring uses them yet. The site's Markdown rendering is unchanged.For the reader
Every quotation in the PDF now prints as a quotation: Acts 2:38 in Spirit baptism, the quotations across the sola fide chapters, and LST §3 in the Triune God chapter (checked by eye on the rendered page, p. 629). The site's pages do not change.
Checks run
lake build,lake build TestimonyTools,lake lint,lake exe axiom-audit(library)python3 scripts/testimony_lint.pyarguments/, andscripts/kernel-replay.shfor both packagesbibgen,statusgen,argdoc,argtex, each with--check;exampletex --checkinexamples/arguments.texwithtectonicand looked at the Trinity quotationtectonicprinted "errors were issued by BibTeX, but were ignored". This PR does not touch the bibliography, and I did not compare this warning againstmain.Sources
None.
Generated by Claude Code