feat: manually highlight keywords

leanprover · Mar 20, 2024 · 4edc491 · 4edc491
1 parent f325880
commit 4edc491
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 2 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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 {{ <code class="hl lean inline" "data-lean-context"={{toString contextName}}> {{ hls.toHtml }} </code> }}
+  | .customHighlight hls, _contents => do
+    pure {{ <code class="hl lean inline"> {{ hls.toHtml }} </code> }}
   | .label x, contents => do
     let contentHtml ← contents.mapM go
     let st ← stateEq ▸ state