From a10a5335baae0aa3d80cf71228f421fe4c9f77e8 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 22 Jul 2022 13:47:47 +0200
Subject: [PATCH] fix: do not highlight module docstrings

Fixes #1353
---
 src/Lean/Server/FileWorker/RequestHandling.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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