Skip to content

add checkmark for leanok command in print mode#77

Open
acmepjz wants to merge 1 commit into
PatrickMassot:masterfrom
acmepjz:acmepjz_checkmark
Open

add checkmark for leanok command in print mode#77
acmepjz wants to merge 1 commit into
PatrickMassot:masterfrom
acmepjz:acmepjz_checkmark

Conversation

@acmepjz

@acmepjz acmepjz commented Sep 7, 2025

Copy link
Copy Markdown

... to align with web mode behavior. Personally I think it looks good.

@PatrickMassot

Copy link
Copy Markdown
Owner

I’m a bit worried that this would make the checkmark appear in a random place since people don’t expect this command to have some pdf output and its precise placement doesn’t matter to plasTeX. Do you have examples of well-known blueprints rendered with this modification?

@acmepjz

acmepjz commented Dec 22, 2025

Copy link
Copy Markdown
Author

Maybe you can see here https://acmepjz.github.io/lean-iwasawa/blueprint/sect0003.html#pseudo-null-criterion and the corresponding pdf file https://acmepjz.github.io/lean-iwasawa/blueprint.pdf (proposition 3.6, around page 5)

... this would make the checkmark appear in a random place since people don’t expect this command to have some pdf output and its precise placement doesn’t matter to plasTeX.

Yes you're right. In the web output, the checkmark always appeared in the beginning of the proposition. This would be also true for pdf if the \leanok command is in the beginning of proposition body (but not at the end, for example).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants