From fd167d6d78d2085e86a0bbbd18d37f732e9d1396 Mon Sep 17 00:00:00 2001 From: Li-yao Xia Date: Mon, 28 Oct 2024 18:35:18 +0100 Subject: [PATCH] syntax: Highlight Goal in any context --- client/syntax/coq.tmLanguage.json | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/client/syntax/coq.tmLanguage.json b/client/syntax/coq.tmLanguage.json index c1adc9c4..a4ae11ca 100644 --- a/client/syntax/coq.tmLanguage.json +++ b/client/syntax/coq.tmLanguage.json @@ -15,7 +15,7 @@ "name": "keyword.control.import.coq" }, { - "match": "\\b(Theorem|Lemma|Remark|Fact|Corollary|Property|Proposition|Goal)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)", + "match": "\\b(Theorem|Lemma|Remark|Fact|Corollary|Property|Proposition)\\s+((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)", "comment": "Theorem declarations", "captures": { "1": { @@ -26,6 +26,10 @@ } } }, + { + "match": "\\bGoal\\b", + "name": "keyword.source.coq" + }, { "match": "\\b(Parameters?|Axioms?|Conjectures?|Variables?|Hypothesis|Hypotheses)(\\s+Inline)?\\b\\s*\\(?\\s*((\\p{L}|[_\\u00A0])(\\p{L}|[0-9_\\u00A0'])*)", "comment": "Assumptions",