chore: adapt Highlighted type

Author: Vtec234

src/verso-blog/VersoBlog.lean

@@ -325,7 +325,7 @@ meta def leanCommand : BlockCommandOf LeanCommandConfig
     let projectExamples ← getSubproject project
     let (_, {highlighted := hls, original := str, ..}) ← projectExamples.getOrSuggest exampleName
     Verso.Hover.addCustomHover exampleName s!"```lean\n{str}\n```"
-    `(Block.other (Blog.BlockExt.highlightedCode { contextName := $(quote project.getId), showProofStates := $(quote showProofStates) } (SubVerso.Highlighting.Highlighted.seq $(quote hls))) #[Block.code $(quote str)])
+    `(Block.other (Blog.BlockExt.highlightedCode { contextName := $(quote project.getId), showProofStates := $(quote showProofStates) } $(quote hls)) #[Block.code $(quote str)])
 
 structure LeanCommandAtArgs where
   project : Ident
@@ -402,7 +402,7 @@ meta def leanTerm : RoleExpanderOf LeanTermArgs
     let projectExamples ← getSubproject project
     let (_, {highlighted := hls, original := str, ..}) ← projectExamples.getOrSuggest <| mkIdentFrom name exampleName
     Verso.Hover.addCustomHover arg s!"```lean\n{str}\n```"
-    `(Inline.other (Blog.InlineExt.highlightedCode { contextName := $(quote project.getId) } (SubVerso.Highlighting.Highlighted.seq $(quote hls))) #[Inline.code $(quote str)])
+    `(Inline.other (Blog.InlineExt.highlightedCode { contextName := $(quote project.getId) } $(quote hls)) #[Inline.code $(quote str)])
   | _, more =>
     if h : more.size > 0 then
       throwErrorAt more[0] "Unexpected contents"

src/verso-manual/VersoManual/InlineLean/Signature.lean

@@ -87,7 +87,7 @@ meta def signature : CodeBlockExpanderOf SignatureConfig
       try
         let ((hls, _, _, _), st') ← ((SubVerso.Examples.checkSignature name sig).run cmdCtx).run cmdState
         setInfoState st'.infoState
-        pure (Highlighted.seq hls)
+        pure hls
       catch e =>
         let fmt ← PrettyPrinter.ppSignature (TSyntax.mk name.raw[0]).getId
         Suggestion.saveSuggestion str (fmt.fmt.pretty 60) (fmt.fmt.pretty 30 ++ "\n")