fix: do not highlight module docstrings

Fixes #1353
2022-07-22 13:47:47 +02:00 · 2022-07-22 13:47:47 +02:00 · a10a5335ba
commit a10a5335ba
parent 4d5515ab0c
1 changed files with 2 additions and 1 deletions
--- 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