diff --git a/package-lock.json b/package-lock.json
index f3c0191ae8c6460394b34b7c507be80add2cdfc6..18b08e455b1ce0a110dcd83ddd0ac65b1c0afebb 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -77,9 +77,9 @@
}
},
"@types/node": {
- "version": "14.0.27",
- "resolved": "https://registry.npmjs.org/@types/node/-/node-14.0.27.tgz",
- "integrity": "sha512-kVrqXhbclHNHGu9ztnAwSncIgJv/FaxmzXJvGXNdcCpV1b8u1/Mi6z6m0vwy0LzKeXFTPLH0NzwmoJ3fNCIq0g=="
+ "version": "14.6.0",
+ "resolved": "https://registry.npmjs.org/@types/node/-/node-14.6.0.tgz",
+ "integrity": "sha512-mikldZQitV94akrc4sCcSjtJfsTKt4p+e/s0AGscVA6XArQ9kFclP+ZiYUMnq987rc6QlYxXv/EivqlfSLxpKA=="
},
"@types/stream-to-array": {
"version": "2.3.0",
@@ -98,9 +98,9 @@
}
},
"@types/vscode": {
- "version": "1.47.0",
- "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.47.0.tgz",
- "integrity": "sha512-nJA37ykkz9FYA0ZOQUSc3OZnhuzEW2vUhUEo4MiduUo82jGwwcLfyvmgd/Q7b0WrZAAceojGhZybg319L24bTA=="
+ "version": "1.48.0",
+ "resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.48.0.tgz",
+ "integrity": "sha512-sZJKzsJz1gSoFXcOJWw3fnKl2sseUgZmvB4AJZS+Fea+bC/jfGPVhmFL/FfQHld/TKtukVONsmoD3Pkyx9iadg=="
},
"@typescript-eslint/experimental-utils": {
"version": "2.34.0",
@@ -170,9 +170,9 @@
}
},
"ajv": {
- "version": "6.12.3",
- "resolved": "https://registry.npmjs.org/ajv/-/ajv-6.12.3.tgz",
- "integrity": "sha512-4K0cK3L1hsqk9xIb2z9vs/XU+PGJZ9PNpJRDS9YLzmNdX6jmVPfamLvTJr0aDAusnHyCHO6MjzlkAsgtqp9teA==",
+ "version": "6.12.4",
+ "resolved": "https://registry.npmjs.org/ajv/-/ajv-6.12.4.tgz",
+ "integrity": "sha512-eienB2c9qVQs2KWexhkrdMLVDoIQCz5KSeLxwg9Lzk4DOfBtIK9PQwwufcsn1jjGuf9WZmqPMbGxOzfcuphJCQ==",
"dev": true,
"requires": {
"fast-deep-equal": "^3.1.1",
@@ -587,9 +587,9 @@
"dev": true
},
"eslint": {
- "version": "7.6.0",
- "resolved": "https://registry.npmjs.org/eslint/-/eslint-7.6.0.tgz",
- "integrity": "sha512-QlAManNtqr7sozWm5TF4wIH9gmUm2hE3vNRUvyoYAa4y1l5/jxD/PQStEjBMQtCqZmSep8UxrcecI60hOpe61w==",
+ "version": "7.7.0",
+ "resolved": "https://registry.npmjs.org/eslint/-/eslint-7.7.0.tgz",
+ "integrity": "sha512-1KUxLzos0ZVsyL81PnRN335nDtQ8/vZUD6uMtWbF+5zDtjKcsklIi78XoE0MVL93QvWTu+E5y44VyyCsOMBrIg==",
"dev": true,
"requires": {
"@babel/code-frame": "^7.0.0",
@@ -630,25 +630,10 @@
"v8-compile-cache": "^2.0.3"
},
"dependencies": {
- "eslint-utils": {
- "version": "2.1.0",
- "resolved": "https://registry.npmjs.org/eslint-utils/-/eslint-utils-2.1.0.tgz",
- "integrity": "sha512-w94dQYoauyvlDc43XnGB8lU3Zt713vNChgt4EWwhXAP2XkBvndfxF0AgIqKOOasjPIPzj9JqgwkwbCYD0/V3Zg==",
- "dev": true,
- "requires": {
- "eslint-visitor-keys": "^1.1.0"
- }
- },
- "eslint-visitor-keys": {
- "version": "1.3.0",
- "resolved": "https://registry.npmjs.org/eslint-visitor-keys/-/eslint-visitor-keys-1.3.0.tgz",
- "integrity": "sha512-6J72N8UNa462wa/KFODt/PJ3IU60SDpC3QXC1Hjc1BXXpfL2C9R5+AU7jhe0F6GREqVMh4Juu+NY7xn+6dipUQ==",
- "dev": true
- },
"lodash": {
- "version": "4.17.19",
- "resolved": "https://registry.npmjs.org/lodash/-/lodash-4.17.19.tgz",
- "integrity": "sha512-JNvd8XER9GQX0v2qJgsaN/mzFCNA5BRe/j8JN9d+tWyGLSodKQHKFicdwNYzWwI3wjRnaKPsGj1XkBjx/F96DQ==",
+ "version": "4.17.20",
+ "resolved": "https://registry.npmjs.org/lodash/-/lodash-4.17.20.tgz",
+ "integrity": "sha512-PlhdFcillOINfeV7Ni6oF1TAEayyZBoZ8bcshTHqOYJYlrqzRK5hagpagky5o4HfCzzd1TRkXPMFq6cKk9rGmA==",
"dev": true
},
"semver": {
@@ -685,22 +670,14 @@
"dev": true
},
"espree": {
- "version": "7.2.0",
- "resolved": "https://registry.npmjs.org/espree/-/espree-7.2.0.tgz",
- "integrity": "sha512-H+cQ3+3JYRMEIOl87e7QdHX70ocly5iW4+dttuR8iYSPr/hXKFb+7dBsZ7+u1adC4VrnPlTkv0+OwuPnDop19g==",
+ "version": "7.3.0",
+ "resolved": "https://registry.npmjs.org/espree/-/espree-7.3.0.tgz",
+ "integrity": "sha512-dksIWsvKCixn1yrEXO8UosNSxaDoSYpq9reEjZSbHLpT5hpaCAKTLBwq0RHtLrIr+c0ByiYzWT8KTMRzoRCNlw==",
"dev": true,
"requires": {
- "acorn": "^7.3.1",
+ "acorn": "^7.4.0",
"acorn-jsx": "^5.2.0",
"eslint-visitor-keys": "^1.3.0"
- },
- "dependencies": {
- "eslint-visitor-keys": {
- "version": "1.3.0",
- "resolved": "https://registry.npmjs.org/eslint-visitor-keys/-/eslint-visitor-keys-1.3.0.tgz",
- "integrity": "sha512-6J72N8UNa462wa/KFODt/PJ3IU60SDpC3QXC1Hjc1BXXpfL2C9R5+AU7jhe0F6GREqVMh4Juu+NY7xn+6dipUQ==",
- "dev": true
- }
}
},
"esprima": {
@@ -719,9 +696,9 @@
},
"dependencies": {
"estraverse": {
- "version": "5.1.0",
- "resolved": "https://registry.npmjs.org/estraverse/-/estraverse-5.1.0.tgz",
- "integrity": "sha512-FyohXK+R0vE+y1nHLoBM7ZTyqRpqAlhdZHCWIWEviFLiGB8b04H6bQs8G+XTthacvT8VuwvteiP7RJSxMs8UEw==",
+ "version": "5.2.0",
+ "resolved": "https://registry.npmjs.org/estraverse/-/estraverse-5.2.0.tgz",
+ "integrity": "sha512-BxbNGGNm0RyRYvUdHpIwv9IWzeM9XClbOxwoATuFdOE7ZE6wHL+HQ5T8hoPM+zHvmKzzsEqhgy0GrQ5X13afiQ==",
"dev": true
}
}
diff --git a/package.json b/package.json
index 850e395b6c9c5fe803627b23ffd5a26b9edad716..8dccddaa87e9a405c4b312f2afff4857c11eab39 100644
--- a/package.json
+++ b/package.json
@@ -23,7 +23,8 @@
"ProB"
],
"activationEvents": [
- "onLanguage:classicalb"
+ "onLanguage:classicalb",
+ "onLanguage:rmchAddOn"
],
"main": "./out/extension",
"contributes": {
@@ -96,12 +97,23 @@
".mch",
".def",
".imp",
- ".ref"
+ ".ref",
+ ".rmch"
],
"aliases": [
"B",
"classical B"
]
+ },
+ {
+ "id": "rmchAddOn",
+ "extensions": [
+ ".rmch"
+ ],
+ "aliases": [
+ "B",
+ "B DSL"
+ ]
}
],
"grammars": [
@@ -109,12 +121,28 @@
"language": "classicalb",
"scopeName": "source.classicalb",
"path": "./syntaxes/classicalb.tmLanguage.json"
+ },
+ {
+ "language": "rmchAddOn",
+ "scopeName": "source.rmchAddOn",
+ "path": "./syntaxes/rmchAddOn.tmLanguage.json"
}
],
"snippets": [
{
"language": "classicalb",
"path": "./snippets/classicalb_snippets.json"
+ },
+ {
+ "language": "rmchAddOn",
+ "path": "./snippets/rmchAddOn_snippets.json"
+ }
+ ],
+ "iconThemes": [
+ {
+ "id": "b",
+ "label": "B",
+ "path": "./themes/b-themes.json"
}
]
},
@@ -127,16 +155,16 @@
},
"devDependencies": {
"@types/mocha": "^7.0.2",
- "@types/node": "^14.0.27",
+ "@types/node": "^14.6.0",
"@typescript-eslint/parser": "^2.34.0",
- "eslint": "^7.6.0",
+ "eslint": "^7.7.0",
"mocha": "^7.2.0",
"typescript": "^3.9.7"
},
"dependencies": {
"@types/ndjson": "^1.5.0",
"@types/stream-to-array": "^2.3.0",
- "@types/vscode": "^1.47.0",
+ "@types/vscode": "^1.48.0",
"b-language-server": "https://github.com/SeeBasTStick/b-language-server/archive/v1.3.3.tar.gz",
"clean": "^4.0.2",
"error": "^10.4.0",
diff --git a/snippets/rmchAddOn_snippets.json b/snippets/rmchAddOn_snippets.json
new file mode 100644
index 0000000000000000000000000000000000000000..59686715dee3cc333fafcfa66c2acaf4251cd607
--- /dev/null
+++ b/snippets/rmchAddOn_snippets.json
@@ -0,0 +1,132 @@
+{
+ ".source.rmchAddOn": {
+ "MACHINE": {
+ "prefix": "RULES_MACHINE ...",
+ "body": "RULES_MACHINE ${1:MyMachine} OPERATIONS \n RULE ${2:test} \n BODY \n RULE_FORALL ${3:x} \n WHERE ${4:x:1..10} \n EXPECT ${5:x*2 = x+x} \n COUNTEREXAMPLE //\"violation of law\" END\nEND//MACHINE"
+ },
+ "package pragma": {
+ "prefix": "package",
+ "body": "/*@package ${1:foo.bar} */"
+ },
+ "import-package pragma": {
+ "prefix": "import-package",
+ "body": "/*@import-package ${1:foo.bazz} */"
+ },
+ "OPERATIONS Keyword": {
+ "prefix": "OPERATIONS",
+ "body": "OPERATIONS"
+ },
+ "DEFINITIONS Keyword": {
+ "prefix": "DEFINITIONS",
+ "body": "DEFINITIONS"
+ },
+ "VARIABLES": {
+ "prefix": "VARIABLES",
+ "body": "VARIABLES\n\t${1:x}\nINVARIANT\n\t${2:P}\nINITIALISATION\n\t${4:I}"
+ },
+ "CONSTANTS": {
+ "prefix": "CONSTANTS",
+ "body": "CONSTANTS\n\t${1:c}\nPROPERTIES\n\t${2:P}"
+ },
+ "ASSERTIONS": {
+ "prefix": "ASSERTIONS",
+ "body": "ASSERTIONS\n\t${1:a}"
+ },
+ "WHILE": {
+ "prefix": "while",
+ "body": "WHILE ${1:p}\nDO\n\t${2:G}\nINVARIANT ${3:Q}\nVARIANT ${4:E}\nEND"
+ },
+ "PRE Template": {
+ "prefix": "PRE",
+ "body": "PRE ${1:p}\nTHEN\n\t${2:G}\nEND"
+ },
+ "VAR": {
+ "prefix": "var",
+ "body": "VAR ${1:z}\nIN\n\t${2:G}\nEND"
+ },
+ "ANY": {
+ "prefix": "any",
+ "body": "ANY ${1:z}\nWHERE\n\t${2:P}\nTHEN\n\t${3:G}\nEND"
+ },
+ "LET": {
+ "prefix": "let",
+ "body": "LET ${1:x}\nBE ${2:E}\nIN\n\t${3:G}\nEND"
+ },
+ "IF": {
+ "prefix": "if",
+ "body": "IF ${1:p}\nTHEN\n\t${2:G}\nEND"
+ },
+ "IF ... ELSE": {
+ "prefix": "ifelse",
+ "body": "IF ${1:p}\nTHEN\n\t${2:G}\nELSE\n\t${2:H}\nEND"
+ },
+ "CHOICE": {
+ "prefix": "choice",
+ "body": "CHOICE\n\t${1:G}\nOR\n\t${2:H}\nEND"
+ },
+ "SELECT": {
+ "prefix": "select",
+ "body": "SELECT\n\t${1:p}\nTHEN\n\t${2:G}\nEND"
+ },
+ "SELECT ... ELSE": {
+ "prefix": "selectelse",
+ "body": "SELECT ${1:p}\nTHEN\n\t${2:G}\nWHEN ${3:q}\nTHEN\n\t${4:H}\nELSE\n\t${5:E}\nEND"
+ },
+ "CASE": {
+ "prefix": "choice",
+ "body": "CHOICE\n\t${1:G}\nOR\n\t${2:H}\nEND"
+ },
+ "Set Pref MININT": {
+ "prefix": "set minint",
+ "body": "SET_PREF_MININT == ${1:n};"
+ },
+ "Set Pref MAXINT": {
+ "prefix": "set minint",
+ "body": "SET_PREF_MININT == ${1:n};"
+ },
+ "B:INT": {
+ "prefix": "INT",
+ "body": "INT;"
+ },
+ "B:INTEGER": {
+ "prefix": "INTEGER",
+ "body": "INTEGER"
+ },
+ "B:NAT": {
+ "prefix": "NAT",
+ "body": "NAT"
+ },
+ "B:NATURAL": {
+ "prefix": "NATURAL",
+ "body": "NATURAL"
+ },
+ "B: -->": {
+ "prefix": "funcTotal",
+ "body": "-->"
+ },
+ "B: >->": {
+ "prefix": "funcTotalInjection",
+ "body": ">->"
+ },
+ "B: -->>": {
+ "prefix": "funcTotalSurjection",
+ "body": ">->"
+ },
+ "B: >->>": {
+ "prefix": "funcTotalBijection",
+ "body": ">->>"
+ },
+ "B: +->": {
+ "prefix": "funcPartial",
+ "body": "+->"
+ },
+ "B: >+>": {
+ "prefix": "funcPartialInjection",
+ "body": "+->>"
+ },
+ "B: >+>>": {
+ "prefix": "funcBijection",
+ "body": ">+>>"
+ }
+ }
+ }
\ No newline at end of file
diff --git a/src/extension.ts b/src/extension.ts
index 69ccdab9b09b0bbbdae69ef47b6e80869b757d64..1bff34c9064e49f7d43102850efd9f9ed3b143e2 100644
--- a/src/extension.ts
+++ b/src/extension.ts
@@ -12,7 +12,6 @@ import {
LanguageClientOptions,
ServerOptions,
} from 'vscode-languageclient';
-import fs from "fs"
import * as path from 'path'
@@ -37,7 +36,7 @@ export function activate(context: ExtensionContext) {
// Options to control the language client
let clientOptions: LanguageClientOptions = {
// Register the server for B files
- documentSelector: [{ scheme: 'file', language: 'classicalb' }],
+ documentSelector: [{ scheme: 'file', language: 'classicalb' }, { scheme: 'file', language: 'rmchAddOn' }],
synchronize: {
// Notify the server about file changes to '.clientrc files contained in the workspace
fileEvents: workspace.createFileSystemWatcher('**/.clientrc')
diff --git a/syntaxes/classicalb.tmLanguage.json b/syntaxes/classicalb.tmLanguage.json
index 05faf12dc548e74aed7145ff9f0c92f288f9dccc..6c6dc78d2b4c6d2a99a0eb58804ef534a24cfa25 100644
--- a/syntaxes/classicalb.tmLanguage.json
+++ b/syntaxes/classicalb.tmLanguage.json
@@ -131,7 +131,7 @@
"machineclauses": {
"patterns": [
{
- "match": "(?x)\n\\b(INITIALIZATION|INITIALISATION|ASSERTIONS|OPERATIONS|SEES|PROMOTES|USES\n|INCLUDES|IMPORTS|REFINES|EXTENDS|INVARIANT|CONCRETE_VARIABLES\n|ABSTRACT_VARIABLES|VARIABLES|PROPERTIES|CONSTANTS|ABSTRACT_CONSTANTS\n|CONCRETE_CONSTANTS|CONSTRAINTS|SETS|DEFINITIONS|VALUES)\\b",
+ "match": "(?x)\n\\b(INITIALI(Z|S)ATION|ASSERTIONS|OPERATIONS|SEES|PROMOTES|USES\n|INCLUDES|IMPORTS|REFINES|EXTENDS|INVARIANT|CONCRETE_VARIABLES\n|ABSTRACT_VARIABLES|VARIABLES|PROPERTIES|CONSTANTS|ABSTRACT_CONSTANTS\n|CONCRETE_CONSTANTS|CONSTRAINTS|SETS|DEFINITIONS|VALUES|GOAL)\\b",
"name": "storage.type.clause.classicalb"
}
]
diff --git a/syntaxes/rmchAddOn.tmLanguage.json b/syntaxes/rmchAddOn.tmLanguage.json
new file mode 100644
index 0000000000000000000000000000000000000000..b40d73a9174e550f57b6f953d3003addf3080dfd
--- /dev/null
+++ b/syntaxes/rmchAddOn.tmLanguage.json
@@ -0,0 +1,367 @@
+{
+ "name": "Rules Machine B",
+ "scopeName": "source.rmchAddOn",
+ "patterns": [
+ {
+ "include": "source.rmchAddOn.rules"
+ },
+ {
+ "include": "#pragma"
+ },
+ {
+ "include": "#comments"
+ },
+ {
+ "include": "#strings"
+ },
+ {
+ "include": "#components"
+ },
+ {
+ "include": "#machineclauses"
+ },
+ {
+ "include": "#control_blocks"
+ },
+ {
+ "include": "#scope_blocks"
+ },
+ {
+ "include": "#keyword_control"
+ },
+ {
+ "include": "#keyword_operators"
+ },
+ {
+ "include": "#constant_values"
+ },
+ {
+ "include": "#preferences"
+ },
+ {
+ "include": "#identifiers"
+ },
+ {
+ "include": "#invalid"
+ },
+ {
+ "include": "#scope_blocks"
+ }
+ ],
+ "repository": {
+ "identifiers": {
+ "patterns": [
+ {
+ "match": "\\b[a-zA-Z][a-zA-Z0-9_]*\\b",
+ "name": "identifier.rmchAddOn"
+ }
+ ]
+ },
+ "pragma": {
+ "patterns": [
+ {
+ "begin": "/\\*@\\b(package|import-package|import_package|symbolic|unit|label|desc|description|conversion|file)\\b",
+ "captures": {
+ "0": {
+ "name": "punctuation.definition.tag.rmchAddOn"
+ }
+ },
+ "end": "\\*/",
+ "name": "identifier.rmchAddOn"
+ }
+ ]
+ },
+ "comments": {
+ "patterns": [
+ {
+ "begin": "/\\*",
+ "captures": {
+ "0": {
+ "name": "punctuation.definition.comment.rmchAddOn"
+ }
+ },
+ "end": "\\*/",
+ "name": "comment.block.rmchAddOn"
+ },
+ {
+ "begin": "//",
+ "captures": {
+ "0": {
+ "name": "punctuation.definition.comment.rmchAddOn"
+ }
+ },
+ "end": "\n",
+ "name": "comment.line.rmchAddOn"
+ }
+ ]
+ },
+ "strings": {
+ "patterns": [
+ {
+ "begin": "\"",
+ "beginCaptures": {
+ "0": {
+ "name": "punctuation.definition.string.begin.rmchAddOn"
+ }
+ },
+ "end": "\"",
+ "endCaptures": {
+ "0": {
+ "name": "punctuation.definition.string.end.rmchAddOn"
+ }
+ },
+ "name": "string.quoted.double.rmchAddOn",
+ "patterns": [
+ {
+ "match": "\\\\.",
+ "name": "constant.character.escape.rmchAddOn"
+ },
+ {
+ "match": "\"\"",
+ "name": "constant.character.escape.quote.rmchAddOn"
+ }
+ ]
+ },
+ {
+ "begin": "'''",
+ "captures": {
+ "0": {
+ "name": "punctuation.definition.string.begin.rmchAddOn"
+ }
+ },
+ "end": "'''",
+ "name": "string.quoted.triple.rmchAddOn"
+ }
+ ]
+ },
+ "machineclauses": {
+ "patterns": [
+ {
+ "match": "(?x)\n\\b(INITIALI(Z|S)ATION|ASSERTIONS|OPERATIONS|SEES|PROMOTES|USES\n|INCLUDES|IMPORTS|REFINES|EXTENDS|INVARIANT|CONCRETE_VARIABLES\n|ABSTRACT_VARIABLES|VARIABLES|PROPERTIES|CONSTANTS|ABSTRACT_CONSTANTS\n|CONCRETE_CONSTANTS|CONSTRAINTS|SETS|DEFINITIONS|VALUES)\\b",
+ "name": "storage.type.clause.rmchAddOn"
+ }
+ ]
+ },
+ "keyword_control": {
+ "patterns": [
+ {
+ "match": "(?x)\n\\b(skip|BE|DO|VARIANT|ELSIF|THEN|ELSE|EITHER|CASE|SELECT\n|ASSERT|WHERE|OR|OF|IN|BODY|GOAL|RULEID|WHEN|COUNTEREXAMPLE|TYPE|VALUE|EXPECT|STRING_FORMAT|DEPENDS_ON_RULE|ERROR_TYPE|ERROR_TYPES|PRECONDITION|POSTCONDITION|DUMMY_VALUE)\\b",
+ "name": "keyword.control.rmchAddOn"
+ }
+ ]
+ },
+ "keyword_operators": {
+ "patterns": [
+ {
+ "match": "\\bnot\\b|¬|\\bor\\b|∨",
+ "name": "keyword.operator.logical.rmchAddOn"
+ },
+ {
+ "match": "!|#|∀|∃|&|∧|<=>|=>|⇔|⇒",
+ "name": "keyword.operator.logical.rmchAddOn"
+ },
+ {
+ "match": "≠|/=|=|==",
+ "name": "keyword.operator.equality.rmchAddOn"
+ },
+ {
+ "match": "\\b(first|last|tail|front|rev|seq|seq1|conc)\\b",
+ "name": "keyword.operator.sequence.rmchAddOn"
+ },
+ {
+ "match": "\\b(tree|btree|top|const|rank|father|son|sons|subtree|arity|bin|left|right|sizet|prefix|postfix|mirror|infix)\\b",
+ "name": "keyword.operator.tree.rmchAddOn"
+ },
+ {
+ "match": "\\b(mod|succ|pred)\\b",
+ "name": "keyword.operator.numeric.rmchAddOn"
+ },
+ {
+ "match": "\\b(rec|struct)\\b",
+ "name": "keyword.operator.record.rmchAddOn"
+ },
+ {
+ "match": "\\b(ran|dom|id|prj1|prj2|closure1|closure|interate|fnc|rel)\\b|%|λ",
+ "name": "keyword.operator.relation.rmchAddOn"
+ },
+ {
+ "match": "bool",
+ "name": "keyword.operator.boolean.rmchAddOn"
+ },
+ {
+ "match": "<--|:=|::",
+ "name": "keyword.operator.assignment.rmchAddOn"
+ },
+ {
+ "match": "\\b(INTER|UNION|SIGMA|PI|POW|POW1|union|inter)\\b|⋂|⋃|∑|∏",
+ "name": "keyword.operator.set.rmchAddOn"
+ },
+ {
+ "match": "\\b(min|max|card|size)\\b",
+ "name": "keyword.operator.set.rmchAddOn"
+ },
+ {
+ "match": ":|∈|∉|\\\\/|/\\\\|∪|∩|⊄|⊈|⊂|⊆",
+ "name": "keyword.operator.set.rmchAddOn"
+ },
+ {
+ "begin": "{",
+ "beginCaptures": {
+ "0": {
+ "name": "punctuation.definition.set.begin.rmchAddOn"
+ }
+ },
+ "end": "}",
+ "endCaptures": {
+ "0": {
+ "name": "punctuation.definition.set.end.rmchAddOn"
+ }
+ },
+ "patterns": [
+ {
+ "include": "$self"
+ }
+ ]
+ },
+ {
+ "match": "-->|-->(>)?|>->(>)?|<->|>+>(>)?",
+ "name": "keyword.operator.relation.rmchAddOn"
+ },
+ {
+ "match": "(\\|>(>)?)|((<)?<\\|)|(\\|->)",
+ "name": "keyword.operator.relation.rmchAddOn"
+ },
+ {
+ "match": "↠|↦|⤀|⤖|⇸|⤔|◀|←|→|↔|↣|▶|⇾|⋖|⊗|◁|▷|⇽",
+ "name": "keyword.operator.relation.rmchAddOn"
+ },
+ {
+ "match": "\\|\\|",
+ "name": "keyword.operator.parallel.rmchAddOn"
+ },
+ {
+ "match": ">|<|>=|=<|≤|≥",
+ "name": "keyword.operator.numeric.rmchAddOn"
+ }
+ ]
+ },
+ "constant_values": {
+ "patterns": [
+ {
+ "match": "\\b\\d+",
+ "name": "constant.numeric.rmchAddOn"
+ },
+ {
+ "match": "{}|∅",
+ "name": "constant.set.rmchAddOn"
+ },
+ {
+ "match": "\\b(TRUE|FALSE)\\b",
+ "name": "constant.language.boolean.rmchAddOn"
+ },
+ {
+ "match": "\\b(BOOL|STRING|INT(EGER)?|NAT(URAL)?(1)?|MININT|MAXINT)\\b",
+ "name": "constant.other.sets.rmchAddOn"
+ }
+ ]
+ },
+ "control_blocks": {
+ "patterns": [
+ {
+ "begin": "(?x)\n\\b(BEGIN|PRE|SELECT|ANY|LET|VAR|ASSERT|WHILE|IF|CHOICE|CASE|EITHER|IN)\\b",
+ "beginCaptures": {
+ "0": {
+ "name": "keyword.control.rmchAddOn"
+ }
+ },
+ "end": "\\bEND\\b",
+ "endCaptures": {
+ "0": {
+ "name": "keyword.control.rmchAddOn"
+ }
+ },
+ "patterns": [
+ {
+ "match": "\\bINVARIANT\\b",
+ "name": "keyword.control.rmchAddOn"
+ },
+ {
+ "include": "$self"
+ }
+ ]
+ }
+ ]
+ },
+ "scope_blocks": {
+ "patterns": [
+ {
+ "begin": "(?x)\n\\b(RULE|COMPUTATION|FUNCTION|RULE_FORALL|RULE_FAIL)\\b",
+ "beginCaptures": {
+ "0": {
+ "name": "keyword.control.rmchAddOn"
+ }
+ },
+ "end": "\\bEND\\b",
+ "endCaptures": {
+ "0": {
+ "name": "keyword.control.rmchAddOn"
+ }
+ },
+ "patterns": [
+ {
+ "match": "\\bINVARIANT\\b",
+ "name": "keyword.control.rmchAddOn"
+ },
+ {
+ "include": "$self"
+ }
+ ]
+ }
+ ]
+ },
+ "components": {
+ "patterns": [
+ {
+ "begin": "\\b(RULES_MACHINE)\\b",
+ "beginCaptures": {
+ "0": {
+ "name": "storage.type.machine.start.rmchAddOn"
+ }
+ },
+ "end": "\\bEND\\b",
+ "endCaptures": {
+ "0": {
+ "name": "storage.type.machine.end.rmchAddOn"
+ }
+ },
+ "name": "meta.machine.rmchAddOn",
+ "patterns": [
+ {
+ "include": "$self"
+ }
+ ]
+ }
+ ]
+ },
+ "preferences": {
+ "patterns": [
+ {
+ "match": "(?x)\n\\b(GOAL|SET_PREF_\\w*|FORCE_SYMMETRY_\\w*|GOAL|ANIMATION_FUNCTION_DEFAULT\n|HEURISTIC_FUNCTION|ANIMATION_FUNCTION[0-9]*|ANIMATION_IMG\\w*\n|ANIMATION_STR\\w*|ASSERT_(LTL|CTL)\\w*)\\b",
+ "name": "entity.other.attribute-name.rmchAddOn"
+ }
+ ]
+ },
+ "invalid": {
+ "patterns": [
+ {
+ "match": "@|\\?|€",
+ "name": "invalid.illegal.other.rmchAddOn"
+ },
+ {
+ "match": ";(\\s)*;",
+ "name": "invalid.illegal.other.rmchAddOn"
+ }
+ ]
+ }
+ }
+ }
\ No newline at end of file