feat: allow parts to disable showing inline HTML ToC #444
8000
Conversation
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
|
Thanks! |
david-christiansen
added a commit
that referenced
this pull request
Jun 20, 2025
* feat: show hovers on closing delimiters (#428) Closes #427 * feat: linter for Unicode typography (#430) * chore: adapt to upstream SubVerso improvements (#432) In particular, this fixes highlighting for sorts and improves the display of tactic states. * feat: LinkTargets for Blog Genre and definitions (#431) * fix: parse ` ` correctly (#433) * doc: update README for nightly procedures (#424) * fix: hover for imax had flipped args (#434) * fix: remove obsolete z-index customization for tactic states (#435) * chore: bump SubVerso version (#438) * fix: demo textbook would delete files (#439) It seems that a relative path became absolute. Now it's relative again. * chore: bump SubVerso for bug fixes (#440) * Fix port number for accessing demosite in README.md (#442) * feat: allow parts to disable showing inline HTML ToC (#444) * feat: cross-references between documents (#441) This is a feature inspired by InterSphinx, to allow documents to reference one another. The idea is that the internal cross-references database is placed at a well-known URL, and documents can download and cache it, using it to resolve links. * chore: bump to nightly-2025-06-19 --------- Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com>
david-christiansen
added a commit
that referenced
this pull request
Jun 23, 2025
Contained: * feat: show hovers on closing delimiters (#428) Closes #427 * feat: linter for Unicode typography (#430) * chore: adapt to upstream SubVerso improvements (#432) In particular, this fixes highlighting for sorts and improves the display of tactic states. * feat: LinkTargets for Blog Genre and definitions (#431) * fix: parse ` ` correctly (#433) * doc: update README for nightly procedures (#424) * fix: hover for imax had flipped args (#434) * fix: remove obsolete z-index customization for tactic states (#435) * chore: bump SubVerso version (#438) * fix: demo textbook would delete files (#439) It seems that a relative path became absolute. Now it's relative again. * chore: bump SubVerso for bug fixes (#440) * Fix port number for accessing demosite in README.md (#442) * feat: allow parts to disable showing inline HTML ToC (#444) * feat: cross-references between documents (#441) This is a feature inspired by InterSphinx, to allow documents to reference one another. The idea is that the internal cross-references database is placed at a well-known URL, and documents can download and cache it, using it to resolve links. * feat: add linters for extra markup (#448) In particular, this will help users not get caught on the fact that `*` is different from Markdown. * fix: display multiple authors correctly (#449) * feat: add part generation and info-string checking in Markdown elab (#445) This PR adds the Markdown elaboration features required for error explanations, namely the ability to create `Part`s from Markdown headers, the ability to access infostrings in code-block elaborators, and a "strict" inline code elaboration mode. * feat: linter for missing section tags in manual genre (#450) * fix: respect `none` for section tags in manual genre (#451) * chore: bump to nightly-2025-06-23 --------- Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com>
kim-em
added a commit
that referenced
this pull request
Jun 30, 2025
* feat: components in blog genre (#385) Components bundle together HTML, JS, and CSS. * chore: bump dependencies for nightly-2025-05-08 (#386) * feat: upstream table from reference manual (#387) * feat: generate directives for block components (#388) * chore: document and partially enforce new procedures (#381) * chore: bump to latest SubVerso and Lean nightly (#390) * fix: use correct internal name for table block (#391) * fix: allow list item contents to be on new line (#392) * fix: behavior of SVG tags inside the HTML (#393) * feat: manual genre can display Lean code from external projects (#394) * feat: allow namespace suppression when extracting external code (#395) * chore: remove redundant error mods (#397) SubVerso now retains the fact that they were errors. * feat: use upstream hints infrastructure in errors (#398) * chore: bump to nightly-2025-05-19 (#399) * feat: alternative approach to incrementality (#400) Replaces the Lean command parser with a new one that takes a block at a time, rather than parsing Verso as one giant command and implementing incrementality "by hand". Each Verso block is elaborated to a top-level definition, which makes the checking for `sorry` and errors work the way it should. Without this, the `sorry` warning was emitted in the presence of errors, which was inconsistent with the rest of Lean. This is also a step towards elaborating Verso directly, which will probably improve performance in the future. A diff threshold was added to `leanOutput` in the manual genre to account for differences in IR shown in examples in the reference manual as a result of compiling blocks to separate defs. * feat: generalize external Lean code display (#401) It can now work in many genres, with only an instance declaration needed. In particular, it works in blogs. * fix: also generate document when text is empty (#402) * feat: bundle KaTeX and include by default in manual genre (#403) * fix: external code rebuilds and hints (#404) Prevents spurious rebuilds from subprocesses and repairs broken hint formatting. * feat: suggest code samples based on string contents (#405) * feat: document elaboration hooks (#406) This allows Verso extensions to register things like cleanup functions for internal state that they can't otherwise control (e.g. temporary directories). * chore: bump toolchain to nightly-2025-05-27 * fix: default anchor suggestions to false (#407) * fix: more reliable external module extraction (#408) * fix: incorporate SubVerso improvements to error/tactic spans (#409) * chore: bump to 2025-06-01 (#413) * chore: bump to 2025-06-05 (#423) * feat: show hovers on closing delimiters (#428) Closes #427 * chore: bump to 2025-06-09 * chore: bump nightly-testing to 2025 06 20 and merge main (#447) * feat: show hovers on closing delimiters (#428) Closes #427 * feat: linter for Unicode typography (#430) * chore: adapt to upstream SubVerso improvements (#432) In particular, this fixes highlighting for sorts and improves the display of tactic states. * feat: LinkTargets for Blog Genre and definitions (#431) * fix: parse ` ` correctly (#433) * doc: update README for nightly procedures (#424) * fix: hover for imax had flipped args (#434) * fix: remove obsolete z-index customization for tactic states (#435) * chore: bump SubVerso version (#438) * fix: demo textbook would delete files (#439) It seems that a relative path became absolute. Now it's relative again. * chore: bump SubVerso for bug fixes (#440) * Fix port number for accessing demosite in README.md (#442) * feat: allow parts to disable showing inline HTML ToC (#444) * feat: cross-references between documents (#441) This is a feature inspired by InterSphinx, to allow documents to reference one another. The idea is that the internal cross-references database is placed at a well-known URL, and documents can download and cache it, using it to resolve links. * chore: bump to nightly-2025-06-19 --------- Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> * chore: bump to nightly-2025-06-23 and merge `main` (#452) Contained: * feat: show hovers on closing delimiters (#428) Closes #427 * feat: linter for Unicode typography (#430) * chore: adapt to upstream SubVerso improvements (#432) In particular, this fixes highlighting for sorts and improves the display of tactic states. * feat: LinkTargets for Blog Genre and definitions (#431) * fix: parse ` ` correctly (#433) * doc: update README for nightly procedures (#424) * fix: hover for imax had flipped args (#434) * fix: remove obsolete z-index customization for tactic states (#435) * chore: bump SubVerso version (#438) * fix: demo textbook would delete files (#439) It seems that a relative path became absolute. Now it's relative again. * chore: bump SubVerso for bug fixes (#440) * Fix port number for accessing demosite in README.md (#442) * feat: allow parts to disable showing inline HTML ToC (#444) * feat: cross-references between documents (#441) This is a feature inspired by InterSphinx, to allow documents to reference one another. The idea is that the internal cross-references database is placed at a well-known URL, and documents can download and cache it, using it to resolve links. * feat: add linters for extra markup (#448) In particular, this will help users not get caught on the fact that `*` is different from Markdown. * fix: display multiple authors correctly (#449) * feat: add part generation and info-string checking in Markdown elab (#445) This PR adds the Markdown elaboration features required for error explanations, namely the ability to create `Part`s from Markdown headers, the ability to access infostrings in code-block elaborators, and a "strict" inline code elaboration mode. * feat: linter for missing section tags in manual genre (#450) * fix: respect `none` for section tags in manual genre (#451) * chore: bump to nightly-2025-06-23 --------- Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> * chore: bump nightly testing to 2025-06-24 and merge main (#455) * chore: bump to nightly nightly-2025-06-26 * chore: bump to nightly nightly-2025-06-27 * chore: bump to nightly nightly-2025-06-28 * chore: bump to nightly nightly-2025-06-29 * chore: delete file that shouldn't have been committed * chore: bump to nightly nightly-2025-06-30 * chore: bump toolchain to v4.22.0-rc1 --------- Co-authored-by: David Thrane Christiansen <david@lean-fro.org> Co-authored-by: Sofia Rodrigues <algebraic.sofia+github@gmail.com> Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk> Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>
kim-em
added a commit
that referenced
this pull request
Jun 30, 2025
* feat: components in blog genre (#385) Components bundle together HTML, JS, and CSS. * chore: bump dependencies for nightly-2025-05-08 (#386) * feat: upstream table from reference manual (#387) * feat: generate directives for block components (#388) * chore: document and partially enforce new procedures (#381) * chore: bump to latest SubVerso and Lean nightly (#390) * fix: use correct internal name for table block (#391) * fix: allow list item contents to be on new line (#392) * fix: behavior of SVG tags inside the HTML (#393) * feat: manual genre can display Lean code from external projects (#394) * feat: allow namespace suppression when extracting external code (#395) * chore: remove redundant error mods (#397) SubVerso now retains the fact that they were errors. * feat: use upstream hints infrastructure in errors (#398) * chore: bump to nightly-2025-05-19 (#399) * feat: alternative approach to incrementality (#400) Replaces the Lean command parser with a new one that takes a block at a time, rather than parsing Verso as one giant command and implementing incrementality "by hand". Each Verso block is elaborated to a top-level definition, which makes the checking for `sorry` and errors work the way it should. Without this, the `sorry` warning was emitted in the presence of errors, which was inconsistent with the rest of Lean. This is also a step towards elaborating Verso directly, which will probably improve performance in the future. A diff threshold was added to `leanOutput` in the manual genre to account for differences in IR shown in examples in the reference manual as a result of compiling blocks to separate defs. * feat: generalize external Lean code display (#401) It can now work in many genres, with only an instance declaration needed. In particular, it works in blogs. * fix: also generate document when text is empty (#402) * feat: bundle KaTeX and include by default in manual genre (#403) * fix: external code rebuilds and hints (#404) Prevents spurious rebuilds from subprocesses and repairs broken hint formatting. * feat: suggest code samples based on string contents (#405) * feat: document elaboration hooks (#406) This allows Verso extensions to register things like cleanup functions for internal state that they can't otherwise control (e.g. temporary directories). * chore: bump toolchain to nightly-2025-05-27 * fix: default anchor suggestions to false (#407) * fix: more reliable external module extraction (#408) * fix: incorporate SubVerso improvements to error/tactic spans (#409) * chore: bump to 2025-06-01 (#413) * chore: bump to 2025-06-05 (#423) * feat: show hovers on closing delimiters (#428) Closes #427 * chore: bump to 2025-06-09 * chore: bump nightly-testing to 2025 06 20 and merge main (#447) * feat: show hovers on closing delimiters (#428) Closes #427 * feat: linter for Unicode typography (#430) * chore: adapt to upstream SubVerso improvements (#432) In particular, this fixes highlighting for sorts and improves the display of tactic states. * feat: LinkTargets for Blog Genre and definitions (#431) * fix: parse ` ` correctly (#433) * doc: update README for nightly procedures (#424) * fix: hover for imax had flipped args (#434) * fix: remove obsolete z-index customization for tactic states (#435) * chore: bump SubVerso version (#438) * fix: demo textbook would delete files (#439) It seems that a relative path became absolute. Now it's relative again. * chore: bump SubVerso for bug fixes (#440) * Fix port number for accessing demosite in README.md (#442) * feat: allow parts to disable showing inline HTML ToC (#444) * feat: cross-references between documents (#441) This is a feature inspired by InterSphinx, to allow documents to reference one another. The idea is that the internal cross-references database is placed at a well-known URL, and documents can download and cache it, using it to resolve links. * chore: bump to nightly-2025-06-19 --------- Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> * chore: bump to nightly-2025-06-23 and merge `main` (#452) Contained: * feat: show hovers on closing delimiters (#428) Closes #427 * feat: linter for Unicode typography (#430) * chore: adapt to upstream SubVerso improvements (#432) In particular, this fixes highlighting for sorts and improves the display of tactic states. * feat: LinkTargets for Blog Genre and definitions (#431) * fix: parse ` ` correctly (#433) * doc: update README for nightly procedures (#424) * fix: hover for imax had flipped args (#434) * fix: remove obsolete z-index customization for tactic states (#435) * chore: bump SubVerso version (#438) * fix: demo textbook would delete files (#439) It seems that a relative path became absolute. Now it's relative again. * chore: bump SubVerso for bug fixes (#440) * Fix port number for accessing demosite in README.md (#442) * feat: allow parts to disable showing inline HTML ToC (#444) * feat: cross-references between documents (#441) This is a feature inspired by InterSphinx, to allow documents to reference one another. The idea is that the internal cross-references database is placed at a well-known URL, and documents can download and cache it, using it to resolve links. * feat: add linters for extra markup (#448) In particular, this will help users not get caught on the fact that `*` is different from Markdown. * fix: display multiple authors correctly (#449) * feat: add part generation and info-string checking in Markdown elab (#445) This PR adds the Markdown elaboration features required for error explanations, namely the ability to create `Part`s from Markdown headers, the ability to access infostrings in code-block elaborators, and a "strict" inline code elaboration mode. * feat: linter for missing section tags in manual genre (#450) * fix: respect `none` for section tags in manual genre (#451) * chore: bump to nightly-2025-06-23 --------- Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> * chore: bump nightly testing to 2025-06-24 and merge main (#455) * chore: bump to nightly nightly-2025-06-26 * chore: bump to nightly nightly-2025-06-27 * chore: bump to nightly nightly-2025-06-28 * chore: bump to nightly nightly-2025-06-29 * chore: delete file that shouldn't have been committed * chore: bump to nightly nightly-2025-06-30 * chore: bump toolchain to v4.22.0-rc2 --------- Co-authored-by: David Thrane Christiansen <david@lean-fro.org> Co-authored-by: Sofia Rodrigues <algebraic.sofia+github@gmail.com> Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk> Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>
kim-em
added a commit
that referenced
this pull request
Jul 4, 2025
* feat: components in blog genre (#385) Components bundle together HTML, JS, and CSS. * chore: bump dependencies for nightly-2025-05-08 (#386) * feat: upstream table from reference manual (#387) * feat: generate directives for block components (#388) * chore: document and partially enforce new procedures (#381) * chore: bump to latest SubVerso and Lean nightly (#390) * fix: use correct internal name for table block (#391) * fix: allow list item contents to be on new line (#392) * fix: behavior of SVG tags inside the HTML (#393) * feat: manual genre can display Lean code from external projects (#394) * feat: allow namespace suppression when extracting external code (#395) * chore: remove redundant error mods (#397) SubVerso now retains the fact that they were errors. * feat: use upstream hints infrastructure in errors (#398) * chore: bump to nightly-2025-05-19 (#399) * feat: alternative approach to incrementality (#400) Replaces the Lean command parser with a new one that takes a block at a time, rather than parsing Verso as one giant command and implementing incrementality "by hand". Each Verso block is elaborated to a top-level definition, which makes the checking for `sorry` and errors work the way it should. Without this, the `sorry` warning was emitted in the presence of errors, which was inconsistent with the rest of Lean. This is also a step towards elaborating Verso directly, which will probably improve performance in the future. A diff threshold was added to `leanOutput` in the manual genre to account for differences in IR shown in examples in the reference manual as a result of compiling blocks to separate defs. * feat: generalize external Lean code display (#401) It can now work in many genres, with only an instance declaration needed. In particular, it works in blogs. * fix: also generate document when text is empty (#402) * feat: bundle KaTeX and include by default in manual genre (#403) * fix: external code rebuilds and hints (#404) Prevents spurious rebuilds from subprocesses and repairs broken hint formatting. * feat: suggest code samples based on string contents (#405) * feat: document elaboration hooks (#406) This allows Verso extensions to register things like cleanup functions for internal state that they can't otherwise control (e.g. temporary directories). * chore: bump toolchain to nightly-2025-05-27 * fix: default anchor suggestions to false (#407) * fix: more reliable external module extraction (#408) * fix: incorporate SubVerso improvements to error/tactic spans (#409) * chore: bump to 2025-06-01 (#413) * chore: bump to 2025-06-05 (#423) * feat: show hovers on closing delimiters (#428) Closes #427 * chore: bump to 2025-06-09 * chore: bump nightly-testing to 2025 06 20 and merge main (#447) * feat: show hovers on closing delimiters (#428) Closes #427 * feat: linter for Unicode typography (#430) * chore: adapt to upstream SubVerso improvements (#432) In particular, this fixes highlighting for sorts and improves the display of tactic states. * feat: LinkTargets for Blog Genre and definitions (#431) * fix: parse ` ` correctly (#433) * doc: update README for nightly procedures (#424) * fix: hover for imax had flipped args (#434) * fix: remove obsolete z-index customization for tactic states (#435) * chore: bump SubVerso version (#438) * fix: demo textbook would delete files (#439) It seems that a relative path became absolute. Now it's relative again. * chore: bump SubVerso for bug fixes (#440) * Fix port number for accessing demosite in README.md (#442) * feat: allow parts to disable showing inline HTML ToC (#444) * feat: cross-references between documents (#441) This is a feature inspired by InterSphinx, to allow documents to reference one another. The idea is that the internal cross-references database is placed at a well-known URL, and documents can download and cache it, using it to resolve links. * chore: bump to nightly-2025-06-19 --------- Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> * chore: bump to nightly-2025-06-23 and merge `main` (#452) Contained: * feat: show hovers on closing delimiters (#428) Closes #427 * feat: linter for Unicode typography (#430) * chore: adapt to upstream SubVerso improvements (#432) In particular, this fixes highlighting for sorts and improves the display of tactic states. * feat: LinkTargets for Blog Genre and definitions (#431) * fix: parse ` ` correctly (#433) * doc: update README for nightly procedures (#424) * fix: hover for imax had flipped args (#434) * fix: remove obsolete z-index customization for tactic states (#435) * chore: bump SubVerso version (#438) * fix: demo textbook would delete files (#439) It seems that a relative path became absolute. Now it's relative again. * chore: bump SubVerso for bug fixes (#440) * Fix port number for accessing demosite in README.md (#442) * feat: allow parts to disable showing inline HTML ToC (#444) * feat: cross-references between documents (#441) This is a feature inspired by InterSphinx, to allow documents to reference one another. The idea is that the internal cross-references database is placed at a well-known URL, and documents can download and cache it, using it to resolve links. * feat: add linters for extra markup (#448) In particular, this will help users not get caught on the fact that `*` is different from Markdown. * fix: display multiple authors correctly (#449) * feat: add part generation and info-string checking in Markdown elab (#445) This PR adds the Markdown elaboration features required for error explanations, namely the ability to create `Part`s from Markdown headers, the ability to access infostrings in code-block elaborators, and a "strict" inline code elaboration mode. * feat: linter for missing section tags in manual genre (#450) * fix: respect `none` for section tags in manual genre (#451) * chore: bump to nightly-2025-06-23 --------- Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> * chore: bump nightly testing to 2025-06-24 and merge main (#455) * chore: bump to nightly nightly-2025-06-26 * chore: bump to nightly nightly-2025-06-27 * chore: bump to nightly nightly-2025-06-28 * chore: bump to nightly nightly-2025-06-29 * chore: delete file that shouldn't have been committed * chore: bump to nightly nightly-2025-06-30 * chore: bump toolchain to v4.22.0-rc3 * chore: bump toolchain to v4.22.0-rc3 --------- Co-authored-by: David Thrane Christiansen <david@lean-fro.org> Co-authored-by: Sofia Rodrigues <algebraic.sofia+github@gmail.com> Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk> Co-authored-by: Pim Otte <otte.pim@gmail.com> Co-authored-by: Hanson Char <hanson.char@gmail.com> Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com> Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>
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.
This PR adds the ability for a
Partto disable showing an inline table of contents on a rendered HTML page with anhtmlTocoption. This is necessary for error explanations, since we will render a custom table of explanations with additional metadata rather than using Verso's built-in table of contents.