From 48d65ef677e4785209db7f9d8c3fb1794c3c8848 Mon Sep 17 00:00:00 2001 From: be5invis Date: Sat, 22 Apr 2017 16:20:48 +0800 Subject: [PATCH] fix syntax for quasiquotes used by ER --- syntaxes/idris.json | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/syntaxes/idris.json b/syntaxes/idris.json index f34de69..04c08ea 100644 --- a/syntaxes/idris.json +++ b/syntaxes/idris.json @@ -72,6 +72,7 @@ { "include": "#data_decl" }, { "include": "#function_signature" }, { "include": "#operator" }, + { "include": "#quasiquote" }, { "include": "#infix_function" }, { "include": "#prelude_type" }, { "include": "#delimiter" }, @@ -159,6 +160,7 @@ { "include": "#parameter_type" }, { "include": "#language_const" }, { "include": "#operator" }, + { "include": "#quasiquote" }, { "include": "#infix_function" }, { "include": "#prelude_type" }, { "include": "#delimiter" }, @@ -253,6 +255,41 @@ "name": "keyword.operator.idris", "match": "\\?[-!#\\$%&\\*\\+\\.\\/<=>@\\\\^|~:]+|[-!#\\$%&\\*\\+\\.\\/<=>@\\\\^|~:\\?][-!#\\$%&\\*\\+\\.\\/<=>@\\\\^|~:]*" }, + "quasiquote": { + "name": "meta.quasiquote.idris", + "begin": "`{", + "beginCaptures": { + "0": { + "name": "keyword.operator.quasiquote.idris" + } + }, + "end": "}", + "endCaptures": { + "0": { + "name": "keyword.operator.quasiquote.idris" + } + }, + "patterns": [ + { + "name": "keyword.operator.arrow.idris", + "match": "->" + }, + { "include": "#parameter_type" }, + { "include": "#language_const" }, + { "include": "#operator" }, + { "include": "#quasiquote" }, + { "include": "#infix_function" }, + { "include": "#prelude_type" }, + { "include": "#delimiter" }, + { "include": "#number_nat" }, + { "include": "#number_integer" }, + { "include": "#number_float" }, + { "include": "#unit" }, + { "include": "#string_double" }, + { "include": "#string_single" }, + { "include": "#data_ctor" } + ] + }, "infix_function": { "name": "keyword.operator.function.infix.idris", "begin": "`",