diff --git a/lake-manifest.json b/lake-manifest.json index 2c0dfe4..4955282 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/subverso.git", "type": "git", "subDir": null, - "rev": "ec2ba38cda997ed872f3860ff260501c1110c6da", + "rev": "cd4d0a3d2973bf03862cacf83f3ca3310b05337a", "name": "subverso", "manifestFile": "lake-manifest.json", "inputRev": "main", diff --git a/src/verso-blog/Verso/Genre/Blog.lean b/src/verso-blog/Verso/Genre/Blog.lean index f883db1..5b1b282 100644 --- a/src/verso-blog/Verso/Genre/Blog.lean +++ b/src/verso-blog/Verso/Genre/Blog.lean @@ -267,6 +267,20 @@ def leanCommand : BlockRoleExpander else throwError "Unexpected contents" +@[role_expander leanKw] +def leanKw : RoleExpander + | args, #[arg] => do + ArgParse.run .done args + let `(inline|code{ $kw:str }) := arg + | throwErrorAt arg "Expected code literal with the keyword" + let hl : SubVerso.Highlighting.Highlighted := .token ⟨.keyword none none none, kw.getString⟩ + pure #[← ``(Inline.other (Blog.InlineExt.customHighlight $(quote hl)) #[Inline.code $(quote kw.getString)])] + | _, more => + if h : more.size > 0 then + throwErrorAt more[0] "Unexpected contents" + else + throwError "Unexpected arguments" + @[role_expander leanTerm] def leanTerm : RoleExpander | args, #[arg] => do diff --git a/src/verso-blog/Verso/Genre/Blog/Basic.lean b/src/verso-blog/Verso/Genre/Blog/Basic.lean index cc3e401..e3b56f0 100644 --- a/src/verso-blog/Verso/Genre/Blog/Basic.lean +++ b/src/verso-blog/Verso/Genre/Blog/Basic.lean @@ -24,6 +24,7 @@ deriving Repr inductive InlineExt where | highlightedCode (contextName : Lean.Name) (highlighted : Highlighted) + | customHighlight (highlighted : Highlighted) | label (name : Lean.Name) | ref (name : Lean.Name) | pageref (name : Lean.Name) @@ -633,7 +634,7 @@ def genreBlock (g : Genre) : Blog.BlockExt → Array (Block g) → Blog.Traverse | _, _ => pure none def genreInline (g : Genre) : Blog.InlineExt → Array (Inline g) → Blog.TraverseM (Option (Inline g)) - | .highlightedCode .., _contents => do + | .highlightedCode .., _contents | .customHighlight .., _contents => do modify fun st => {st with stylesheets := st.stylesheets.insert highlightingStyle, scripts := st.scripts.insert highlightingJs diff --git a/src/verso-blog/Verso/Genre/Blog/Template.lean b/src/verso-blog/Verso/Genre/Blog/Template.lean index 8965005..a2ec6c2 100644 --- a/src/verso-blog/Verso/Genre/Blog/Template.lean +++ b/src/verso-blog/Verso/Genre/Blog/Template.lean @@ -183,6 +183,8 @@ def inlineHtml (g : Genre) [MonadConfig (HtmlT g IO)] [MonadPath (HtmlT g IO)] (go : Inline g → HtmlT g IO Html) : Blog.InlineExt → Array (Inline g) → HtmlT g IO Html | .highlightedCode contextName hls, _contents => do pure {{ {{ hls.toHtml }} }} + | .customHighlight hls, _contents => do + pure {{ {{ hls.toHtml }} }} | .label x, contents => do let contentHtml ← contents.mapM go let st ← stateEq ▸ state