diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 208323b607..d0cb015be5 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -298,7 +298,8 @@ def noHighlightKinds : Array SyntaxNodeKind := #[ ``Lean.Parser.Term.prop, -- not really keywords `antiquotName, - ``Lean.Parser.Command.docComment] + ``Lean.Parser.Command.docComment, + ``Lean.Parser.Command.moduleDoc] structure SemanticTokensContext where beginPos : String.Pos