[gtksourceview: 2/5] lean.lang: improve the highlighting of commands




commit 890aed539d1d5942b7b29db81da95f8cca74c504
Author: Elias Aebi <353-eyelash users noreply gitlab gnome org>
Date:   Sat Sep 3 11:50:21 2022 +0200

    lean.lang: improve the highlighting of commands
    
    Commands are not required to start at the beginning of a line.

 data/language-specs/lean.lang | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)
---
diff --git a/data/language-specs/lean.lang b/data/language-specs/lean.lang
index 73fa265e..7a24beba 100644
--- a/data/language-specs/lean.lang
+++ b/data/language-specs/lean.lang
@@ -69,12 +69,12 @@
 
     <context id="command" style-ref="command">
       <match extended="true">
-        ^\s*\#(
+        \#(
             check(_failure)?
           | eval
           | print
           | reduce
-        )
+        )\b
       </match>
     </context>
 


[Date Prev][Date Next]   [Thread Prev][Thread Next]   [Thread Index] [Date Index] [Author Index]