feat: more semantic tokens for Markdown/Verso

src/Lean/Data/Lsp/LanguageFeatures.lean

@@ -454,14 +454,60 @@ inductive SemanticTokenType where
   | decorator
   -- Extensions
   | leanSorryLike
+  -- Markdown/Verso markup highlighting. The composing types combine an
+  -- emphasis subset (none, bold, italic, or both) with a block context (none,
+  -- heading, blockquote, list).
+  | markupBold
+  | markupItalic
+  | markupBoldItalic
+  | markupHeading
+  | markupBoldHeading
+  | markupItalicHeading
+  | markupBoldItalicHeading
+  | markupQuote
+  | markupBoldQuote
+  | markupItalicQuote
+  | markupBoldItalicQuote
+  | markupList
+  | markupBoldList
+  | markupItalicList
+  | markupBoldItalicList
+  | markupInlineCode
+  | markupCodeBlock
+  /--
+  Plain markup text inside a docstring or moduledoc. This is used for Verso or Markdown content that
+  is not otherwise styled, allowing themes to apply the correct style.
+  -/
+  | markupDocText
+  /--
+  Plain markup text outside of a docstring or moduledoc. This is used for Verso or Markdown content
+  that is not otherwise styled in contexts that are not docstrings (such as full-document Verso
+  content), allowing themes to style it the way they would ordinary text content.
+  -/
+  | markupPlainText
+  /--
+  A URL literal in an inline link/image target or autolink.
+  -/
+  | markupUrl
+  /--
+  A cross-reference label: the `[label]` of a link reference definition, or the label part of a
+  reference-style or shortcut link.
+  -/
+  | markupCrossReference
   deriving ToJson, FromJson, BEq, Hashable
 
 -- must be in the same order as the constructors
 def SemanticTokenType.names : Array String :=
   #["keyword", "variable", "property", "function", "namespace", "type", "class",
     "enum", "interface", "struct", "typeParameter", "parameter", "enumMember",
     "event", "method", "macro", "modifier", "comment", "string", "number",
-    "regexp", "operator", "decorator", "leanSorryLike"]
+    "regexp", "operator", "decorator", "leanSorryLike",
+    "markupBold", "markupItalic", "markupBoldItalic",
+    "markupHeading", "markupBoldHeading", "markupItalicHeading", "markupBoldItalicHeading",
+    "markupQuote", "markupBoldQuote", "markupItalicQuote", "markupBoldItalicQuote",
+    "markupList", "markupBoldList", "markupItalicList", "markupBoldItalicList",
+    "markupInlineCode", "markupCodeBlock",
+    "markupDocText", "markupPlainText", "markupUrl", "markupCrossReference"]
 
 def SemanticTokenType.toNat (tokenType : SemanticTokenType) : Nat :=
   tokenType.ctorIdx

src/Lean/Server/FileWorker.lean

@@ -18,6 +18,7 @@ public import Lean.Server.FileWorker.Utils
 public import Lean.Server.FileWorker.RequestHandling
 public import Lean.Server.FileWorker.WidgetRequests
 public import Lean.Server.FileWorker.SetupFile
+public import Lean.Server.FileWorker.Markdown
 public import Lean.Server.Completion.ImportCompletion
 public import Lean.Server.CodeActions.UnknownIdentifier
 

src/Lean/Server/FileWorker/Markdown.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+module
+
+prelude
+public import Lean.Server.FileWorker.Markdown.Basic
+public import Lean.Server.FileWorker.Markdown.Parser
+
+/-!
+# Markdown parser for the language server
+
+A CommonMark parser used by the Lean language server to provide semantic token highlighting inside
+Markdown docstrings. The entry point is `Lean.Server.FileWorker.Markdown.parseDocument`.
+
+The implementation follows CommonMark 0.31.2 closely with a small set of deviations:
+* HTML blocks and inline HTML are not parsed.
+* Link labels are compared case-insensitively only for the English letters A-Z, and case-sensitively
+  for all other characters.
+* Named character entities are not validated against the set of HTML entities.
+-/