[gtksourceview: 2/5] lean.lang: improve the highlighting of commands
- From: Christian Hergert <chergert src gnome org>
- To: commits-list gnome org
- Cc:
- Subject: [gtksourceview: 2/5] lean.lang: improve the highlighting of commands
- Date: Mon, 5 Sep 2022 22:24:53 +0000 (UTC)
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]