Skip to content

Commit

Permalink
Hide bottom toc, and improve math syntax
Browse files Browse the repository at this point in the history
  • Loading branch information
utensil committed Oct 28, 2024
1 parent ce2a6e1 commit dbeaa79
Show file tree
Hide file tree
Showing 3 changed files with 8 additions and 4 deletions.
1 change: 1 addition & 0 deletions lean4-verso-xp/Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ where
config := {
-- destination := "dist",
extraFiles := [("static", "static")],
extraCss := ["/static/overrides.css"],
-- extraCss := ["/static/colors.css", "/static/theme.css", "/static/print.css", "/static/fonts/source-serif/source-serif-text.css", "/static/fonts/source-code-pro/source-code-pro.css", "/static/katex/katex.min.css"],
-- extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"],
extraJs := ["/static/math.js"],
Expand Down
8 changes: 4 additions & 4 deletions lean4-verso-xp/VersoXp/Math.lean
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@ open Lean.MessageSeverity
-- #check Verso.Doc.MathMode

open Verso Doc Elab in
@[code_block_expander latex]
def Manual.latex : CodeBlockExpander
@[code_block_expander math]
def Manual.math: CodeBlockExpander
| _args, str => do
return #[(← `(Doc.Block.para #[Doc.Inline.math Doc.MathMode.display s!"{$str}"]))]

Expand All @@ -32,9 +32,9 @@ $$`E=mc^2`

❌ But no support for multiline math yet.

The following is a workaround inspired by [lecopivo/scientific-computing-lean](https://github.com/lecopivo/scientific-computing-lean/blob/ae7f1f6359465687136a9e75e0c83a1ef19525c2/ScientificComputingInLean/Meta/Latex.lean):
The following is a workaround inspired by [lecopivo/scientific-computing-lean](https://github.com/lecopivo/scientific-computing-lean/blob/ae7f1f6359465687136a9e75e0c83a1ef19525c2/ScientificComputingInLean/Meta/Latex.lean), and the syntax is the same as [one variant of GFM for math](https://docs.github.com/en/get-started/writing-on-github/working-with-advanced-formatting/writing-mathematical-expressions#writing-expressions-as-blocks):

```latex
```math
f'(x) = \lim_{h → 0} \frac{f(x+h) - f(x)}{h}
```

3 changes: 3 additions & 0 deletions lean4-verso-xp/static/overrides.css
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
.section-toc {
display: none;
}

0 comments on commit dbeaa79

Please sign in to comment.