From 4e70b1973e806d50cfb5c07d319ca0de3a731efe Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 15 Dec 2023 11:36:39 +0100 Subject: [PATCH] feat: TeX math --- doc/UsersGuide/Markup.lean | 6 ++ src/leanblog/LeanDoc/Genre/Blog/Basic.lean | 15 +++- src/leanblog/LeanDoc/Genre/Blog/Generate.lean | 2 +- src/leanblog/LeanDoc/Genre/Blog/Template.lean | 5 ++ src/leandoc/LeanDoc/Doc.lean | 7 +- src/leandoc/LeanDoc/Doc/Elab.lean | 14 +++ src/leandoc/LeanDoc/Doc/Html.lean | 3 + src/leandoc/LeanDoc/Doc/TeX.lean | 4 +- src/leandoc/LeanDoc/Output/Html.lean | 6 +- src/leandoc/LeanDoc/Parser.lean | 86 +++++++++++++++++-- src/leandoc/LeanDoc/Syntax.lean | 2 + src/manual/LeanDoc/Genre/Manual.lean | 8 +- 12 files changed, 145 insertions(+), 13 deletions(-) diff --git a/doc/UsersGuide/Markup.lean b/doc/UsersGuide/Markup.lean index 97388b4..7aa346f 100644 --- a/doc/UsersGuide/Markup.lean +++ b/doc/UsersGuide/Markup.lean @@ -33,8 +33,14 @@ Like Markdown, Lean's markup has three primary syntactic categories: ## Description +TODO build an extension to test the parsing here + ### Inline Syntax + + +TeX math can be included using a single or double dollar sign followed by code. Two dollar signs results in display-mode math, so `` $`\sum_{i=0}^{10} i` `` results in $`\sum_{i=0}^{10} i` while `` $$`\sum_{i=0}^{10} i` `` results in: $$`\sum_{i=0}^{10} i` + ### Block Syntax ### Document Structure diff --git a/src/leanblog/LeanDoc/Genre/Blog/Basic.lean b/src/leanblog/LeanDoc/Genre/Blog/Basic.lean index 8ad39da..5482d1d 100644 --- a/src/leanblog/LeanDoc/Genre/Blog/Basic.lean +++ b/src/leanblog/LeanDoc/Genre/Blog/Basic.lean @@ -278,6 +278,16 @@ def highlightingJs : String := } " +def renderMathJs : String := +"document.addEventListener(\"DOMContentLoaded\", () => { + for (const m of document.querySelectorAll(\".math.inline\")) { + katex.render(m.textContent, m, {throwOnError: false, displayMode: false}); + } + for (const m of document.querySelectorAll(\".math.display\")) { + katex.render(m.textContent, m, {throwOnError: false, displayMode: true}); + } +});" + instance : Traverse Blog Blog.TraverseM where part _ := pure () block _ := pure () @@ -285,7 +295,10 @@ instance : Traverse Blog Blog.TraverseM where genrePart _ _ := pure none genreBlock | .highlightedCode .., _contents => do - modify fun st => {st with stylesheets := st.stylesheets.insert highlightingStyle, scripts := st.scripts.insert highlightingJs} + modify fun st => {st with + stylesheets := st.stylesheets.insert highlightingStyle, + scripts := st.scripts.insert highlightingJs + } pure none | _, _ => pure none genreInline diff --git a/src/leanblog/LeanDoc/Genre/Blog/Generate.lean b/src/leanblog/LeanDoc/Genre/Blog/Generate.lean index e150e32..9107d81 100644 --- a/src/leanblog/LeanDoc/Genre/Blog/Generate.lean +++ b/src/leanblog/LeanDoc/Genre/Blog/Generate.lean @@ -25,7 +25,7 @@ def Generate.Context.templateContext (ctxt : Generate.Context) (params : Templat params := params path := ctxt.ctxt.path builtInStyles := ctxt.xref.stylesheets - builtInScripts := ctxt.xref.scripts + builtInScripts := ctxt.xref.scripts.insert Traverse.renderMathJs abbrev GenerateM := ReaderT Generate.Context IO diff --git a/src/leanblog/LeanDoc/Genre/Blog/Template.lean b/src/leanblog/LeanDoc/Genre/Blog/Template.lean index d101648..a924eb7 100644 --- a/src/leanblog/LeanDoc/Genre/Blog/Template.lean +++ b/src/leanblog/LeanDoc/Genre/Blog/Template.lean @@ -205,6 +205,11 @@ def builtinHeader : TemplateM Html := do out := out ++ {{"\n"}} for script in (← read).builtInScripts do out := out ++ {{"\n"}} + out := out ++ {{ + + + }} + pure out namespace Params diff --git a/src/leandoc/LeanDoc/Doc.lean b/src/leandoc/LeanDoc/Doc.lean index 62aba8c..1e94d31 100644 --- a/src/leandoc/LeanDoc/Doc.lean +++ b/src/leandoc/LeanDoc/Doc.lean @@ -41,12 +41,16 @@ instance : Repr Genre.none.Inline where instance : Repr Genre.none.PartMetadata where reprPrec e _ := nomatch e +inductive MathMode where | inline | display +deriving Repr, BEq inductive Inline (genre : Genre) : Type where | text (string : String) | emph (content : Array (Inline genre)) | bold (content : Array (Inline genre)) | code (string : String) + /-- Embedded blobs of TeX math -/ + | math (mode : MathMode) (string : String) | linebreak (string : String) | link (content : Array (Inline genre)) (url : String) | footnote (name : String) (content : Array (Inline genre)) @@ -75,6 +79,7 @@ partial def Inline.reprPrec [Repr g.Inline] (inline : Inline g) (prec : Nat) : S | .emph content => reprCtor ``Inline.emph [reprArray go content] | .bold content => reprCtor ``Inline.bold [reprArray go content] | .code str => reprCtor ``Inline.code [reprArg str] + | .math mode str => reprCtor ``Inline.math [reprArg mode, reprArg str] | .linebreak str => reprCtor ``Inline.linebreak [reprArg str] | .link content dest => reprCtor ``Inline.link [ reprArray go content, @@ -207,7 +212,7 @@ where match ← Traverse.genreInline container content with | .none => .other container <$> content.mapM inline | .some i' => inline i' - | .text .. | .linebreak .. | .code .. => pure i + | .text .. | .linebreak .. | .code .. | .math .. => pure i block (b : Doc.Block g) : m (Doc.Block g) := do Traverse.block b diff --git a/src/leandoc/LeanDoc/Doc/Elab.lean b/src/leandoc/LeanDoc/Doc/Elab.lean index 097987b..3dbe95d 100644 --- a/src/leandoc/LeanDoc/Doc/Elab.lean +++ b/src/leandoc/LeanDoc/Doc/Elab.lean @@ -153,6 +153,20 @@ def _root_.LeanDoc.Syntax.code.expand : InlineExpander ``(Inline.code $s) | _ => throwUnsupportedSyntax + +@[inline_expander LeanDoc.Syntax.inline_math] +def _root_.LeanDoc.Syntax.inline_math.expand : InlineExpander + | `(inline| ${ code{ $s } }) => + ``(Inline.math MathMode.inline $s) + | _ => throwUnsupportedSyntax + +@[inline_expander LeanDoc.Syntax.display_math] +def _root_.LeanDoc.Syntax.display_math.expand : InlineExpander + | `(inline| $${ code{ $s } }) => + ``(Inline.math MathMode.display $s) + | _ => throwUnsupportedSyntax + + def elabBlock (block : Syntax) : DocElabM (TSyntax `term) := withRef block <| withFreshMacroScope <| withIncRecDepth <| do match block with diff --git a/src/leandoc/LeanDoc/Doc/Html.lean b/src/leandoc/LeanDoc/Doc/Html.lean index 18108e4..04484fe 100644 --- a/src/leandoc/LeanDoc/Doc/Html.lean +++ b/src/leandoc/LeanDoc/Doc/Html.lean @@ -82,6 +82,9 @@ partial def Inline.toHtml [Monad m] [GenreHtml g m] : Inline g → HtmlT g m Htm | .bold content => do pure {{ {{← content.mapM toHtml}} }} | .code str => pure {{ {{str}} }} + | .math mode str => do + let classes := "math " ++ match mode with | .inline => "inline" | .display => "display" + pure {{ {{str}} }} | .concat inlines => inlines.mapM toHtml | .other container content => GenreHtml.inline Inline.toHtml container content diff --git a/src/leandoc/LeanDoc/Doc/TeX.lean b/src/leandoc/LeanDoc/Doc/TeX.lean index f36058f..5a62f76 100644 --- a/src/leandoc/LeanDoc/Doc/TeX.lean +++ b/src/leandoc/LeanDoc/Doc/TeX.lean @@ -28,7 +28,7 @@ def logError [Monad m] (message : String) : TeXT g m Unit := do def header [Monad m] (name : TeX) : TeXT g m TeX := do let opts ← options let some i := opts.headerLevel - | logError "No more header nesting available"; return \TeX{\textbf{\Lean{name}}} + | logError s!"No more header nesting available at {name.asString}"; return \TeX{\textbf{\Lean{name}}} let header := opts.headerLevels[i] pure <| .raw (s!"\\{header}" ++ "{") ++ name ++ .raw "}" @@ -62,6 +62,8 @@ partial defmethod Inline.toTeX [Monad m] [GenreTeX g m] : Inline g → TeXT g m pure \TeX{\textbf{\Lean{← content.mapM toTeX}}} | .code str => do pure \TeX{s!"\\verb|{str}|"} --- TODO choose delimiter automatically + | .math .inline str => pure <| .raw s!"${str}$" + | .math .display str => pure <| .raw s!"\\[{str}\\]" | .concat inlines => inlines.mapM toTeX | .other container content => GenreTeX.inline Inline.toTeX container content diff --git a/src/leandoc/LeanDoc/Output/Html.lean b/src/leandoc/LeanDoc/Output/Html.lean index cab31b9..57acb67 100644 --- a/src/leandoc/LeanDoc/Output/Html.lean +++ b/src/leandoc/LeanDoc/Output/Html.lean @@ -145,7 +145,11 @@ partial def asString : Html → String | .text true str => str.replace "<" "<" |>.replace ">" ">" | .text false str => str | .tag name attrs (.seq #[]) => - "<" ++ name ++ attrsAsString attrs ++ "/>" + -- TODO make this more elegant + if name == "script" then + "<" ++ name ++ attrsAsString attrs ++ ">" + else + "<" ++ name ++ attrsAsString attrs ++ "/>" | .tag name attrs (.seq #[subElem]) => "<" ++ name ++ attrsAsString attrs ++ ">" ++ asString subElem ++ s!"" | .tag "pre" attrs body => diff --git a/src/leandoc/LeanDoc/Parser.lean b/src/leandoc/LeanDoc/Parser.lean index 286d91d..f73ec2d 100644 --- a/src/leandoc/LeanDoc/Parser.lean +++ b/src/leandoc/LeanDoc/Parser.lean @@ -304,6 +304,11 @@ Remaining: #guard_msgs in #eval nl.test! "\n " +def fakeAtom (str : String) : ParserFn := fun _c s => + let atom := mkAtom SourceInfo.none str + s.pushSyntax atom + + def strFn (str : String) : ParserFn := asStringFn <| fun c s => let rec go (iter : String.Iterator) (s : ParserState) := if iter.atEnd then s @@ -396,6 +401,22 @@ def inlineTextChar : ParserFn := fun c s => else if c.input.get' i' h == '[' then s.mkUnexpectedErrorAt "![" i else s + | '$' => + let s := s.next' c.input i h + let i' := s.pos + if h : c.input.atEnd i' then + s + else if c.input.get' i' h == '`' then + s.mkUnexpectedErrorAt "$`" i + else if c.input.get' i' h == '$' then + let s := s.next' c.input i' h + let i' := s.pos + if h : c.input.atEnd i' then + s + else if c.input.get' i' h == '`' then + s.mkUnexpectedErrorAt "$$`" i + else s + else s | _ => s.next' c.input i h /-- Return some inline text up to the next inline opener or the end of @@ -820,6 +841,9 @@ mutual else if ch == '\n' then s.mkUnexpectedError "newline" else takeContentsFn maxCount c (s.next' c.input i h) + partial def math : ParserFn := + atomicFn (nodeFn ``display_math <| strFn "$$" >> code >> fakeAtom "`") <|> + atomicFn (nodeFn ``inline_math <| strFn "$" >> code >> fakeAtom "`") -- Read a prefix of a line of text, stopping at a text-mode special character partial def text := @@ -873,7 +897,7 @@ mutual s.pushSyntax fakeClose - partial def delimitedInline (ctxt : InlineCtxt) : ParserFn := emph ctxt <|> bold ctxt <|> code <|> role ctxt <|> image <|> link ctxt <|> footnote ctxt + partial def delimitedInline (ctxt : InlineCtxt) : ParserFn := emph ctxt <|> bold ctxt <|> code <|> math <|> role ctxt <|> image <|> link ctxt <|> footnote ctxt partial def inline (ctxt : InlineCtxt) : ParserFn := text <|> linebreak ctxt <|> delimitedInline ctxt @@ -1215,6 +1239,60 @@ All input consumed. #guard_msgs in #eval inline {} |>.test! "[^1]" +/-- +info: Success! Final stack: + (LeanDoc.Syntax.inline_math + "$" + (LeanDoc.Syntax.code + "`" + (str "\"\\\\frac{x}{4}\"") + "`") + "`") +All input consumed. +-/ +#guard_msgs in +#eval inline {} |>.test! "$`\\frac{x}{4}`" + +/-- +info: Success! Final stack: + (LeanDoc.Syntax.display_math + "$$" + (LeanDoc.Syntax.code + "`" + (str "\"\\\\frac{x}{4}\"") + "`") + "`") +All input consumed. +-/ +#guard_msgs in +#eval inline {} |>.test! "$$`\\frac{x}{4}`" + +/-- +info: Success! Final stack: + (LeanDoc.Syntax.text (str "\"$35.23\"")) +All input consumed. +-/ +#guard_msgs in +#eval inline {} |>.test! "$35.23" + +/-- +info: Success! Final stack: + (LeanDoc.Syntax.text (str "\"$\"")) +Remaining: +"`code`" +-/ +#guard_msgs in +#eval inline {} |>.test! "\\$`code`" + +/-- +info: Success! Final stack: + (LeanDoc.Syntax.text (str "\"$$$\"")) +All input consumed. +-/ +#guard_msgs in +#eval inline {} |>.test! "$$$" + + structure InList where indentation : Nat type : OrderedListType ⊕ UnorderedListType @@ -1226,10 +1304,6 @@ structure BlockCtxt where inLists : List InList := [] deriving Inhabited, Repr -def fakeAtom (str : String) : ParserFn := fun _c s => - let atom := mkAtom SourceInfo.none str - s.pushSyntax atom - def lookaheadOrderedListIndicator (ctxt : BlockCtxt) (p : OrderedListType → Int → ParserFn) : ParserFn := fun c s => let iniPos := s.pos let iniSz := s.stxStack.size @@ -1772,7 +1846,7 @@ All input consumed. #eval blocks {} |>.test! "* foo\n * bar\n* more outer" /-- -info: Failure: unexpected end of input; expected ![, [, [^ or expected beginning of line at ⟨2, 15⟩ +info: Failure: unexpected end of input; expected ![, $, $$, [, [^ or expected beginning of line at ⟨2, 15⟩ Final stack: [(LeanDoc.Syntax.dl [(LeanDoc.Syntax.desc diff --git a/src/leandoc/LeanDoc/Syntax.lean b/src/leandoc/LeanDoc/Syntax.lean index 3777a82..6ac4af4 100644 --- a/src/leandoc/LeanDoc/Syntax.lean +++ b/src/leandoc/LeanDoc/Syntax.lean @@ -38,6 +38,8 @@ syntax (name:=linebreak) "line!" : inline /-- Literal characters-/ syntax (name:=code) "code{" str "}" : inline syntax (name:=role) "role{" ident argument* "}" "[" inline "]" : inline +syntax (name:=inline_math) "${" inline "}" : inline +syntax (name:=display_math) "$${" inline "}" : inline declare_syntax_cat list_item /-- List item -/ diff --git a/src/manual/LeanDoc/Genre/Manual.lean b/src/manual/LeanDoc/Genre/Manual.lean index 327c188..ed798c6 100644 --- a/src/manual/LeanDoc/Genre/Manual.lean +++ b/src/manual/LeanDoc/Genre/Manual.lean @@ -60,12 +60,16 @@ def ensureDir (dir : System.FilePath) : IO Unit := do open IO.FS in def emitTeX (logError : String → IO Unit) (config : Config) (text : Part Manual) : IO Unit := do let opts : TeX.Options Manual IO := {headerLevels := #["chapter", "section", "subsection", "subsubsection", "paragraph"], headerLevel := some ⟨0, by simp_arith [Array.size, List.length]⟩, logError := logError} - let rendered ← text.toTeX (opts, (), ()) + let frontMatter ← text.content.mapM (·.toTeX (opts, (), ())) + let chapters ← text.subParts.mapM (·.toTeX (opts, (), ())) let dir := config.destination.join "tex" ensureDir dir withFile (dir.join "main.tex") .write fun h => do h.putStrLn (preamble text.titleString ["author 1", "author 2"]) - h.putStrLn rendered.asString + for b in frontMatter do + h.putStrLn b.asString + for c in chapters do + h.putStrLn c.asString h.putStrLn postamble def manualMain (text : Part Manual) (options : List String) : IO UInt32 := do