Skip to content

Commit 329b1e8

Browse files
committed
Add toTex support for Manual.keywordOf
1 parent f92bb90 commit 329b1e8

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

Manual/Meta/Syntax.lean

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -125,7 +125,10 @@ def keywordOf : RoleExpander
125125
def keywordOf.descr : InlineDescr where
126126
traverse _ _ _ := do
127127
pure none
128-
toTeX := none
128+
toTeX :=
129+
some <| fun go _id _ content => do
130+
pure <| .seq <| ← content.mapM fun b => do
131+
pure <| .seq #[← go b, .raw "\n"]
129132
toHtml :=
130133
open Verso.Output Html in
131134
some <| fun goI _ info content => do

0 commit comments

Comments
 (0)