fix: render array literals correctly

leanprover · Feb 1, 2024 · 335c4c3 · 335c4c3
1 parent d9e57fd
commit 335c4c3
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 1 deletion.
diff --git a/examples/website/DemoSite/Blog/Conditionals.lean b/examples/website/DemoSite/Blog/Conditionals.lean
@@ -28,4 +28,7 @@ example : Int := if True then 1 else 2
 def slowId : Nat → Nat
   | 0 => 0
   | n + 1 => slowId n + 1
+
+/-- An array literal -/
+example := #[1, 2, 3]
 ```
diff --git a/src/verso-blog/Verso/Genre/Blog/HighlightCode.lean b/src/verso-blog/Verso/Genre/Blog/HighlightCode.lean
@@ -340,7 +340,12 @@ partial def highlight' (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : Syntax)
       else
         emitToken i <| (⟨ ·,  x⟩) <|
         match x.get? 0 with
-        | some '#' => .keyword lookingAt docs
+        | some '#' =>
+          match x.get? ((0 : String.Pos) + '#') with
+          | some c =>
+            if c.isAlpha then .keyword lookingAt docs
+            else .unknown
+          | _ => .unknown
         | some c =>
           if c.isAlpha then .keyword lookingAt docs
           else .unknown