diff --git a/syntax.json b/syntax.json index 0dafe57..8d9a54a 100644 --- a/syntax.json +++ b/syntax.json @@ -812,5 +812,21 @@ } } ] + }, + { + "language": "Agda", + "markers": [ + { + "type": "line", + "pattern": "--" + }, + { + "type": "block", + "pattern": { + "start": "{-", + "end": "-}" + } + } + ] } ]