From a1fca460e5a55eb61c36647e9fc5ad8b22ce2f7d Mon Sep 17 00:00:00 2001 From: SeeBasTStick <sebastian.stock@hhu.de> Date: Wed, 20 May 2020 10:03:45 +0200 Subject: [PATCH] added sound word completion --- server/src/server.ts | 4 + server/src/wordCompletion.ts | 1373 ++++++++++++++++++++++++++++++++-- 2 files changed, 1320 insertions(+), 57 deletions(-) diff --git a/server/src/server.ts b/server/src/server.ts index ef3dee3..6d316f6 100644 --- a/server/src/server.ts +++ b/server/src/server.ts @@ -204,6 +204,10 @@ connection.onCompletion( ); +//Can be used to enrich completion with more infos +connection.onCompletionResolve( + (item : CompletionItem) => {return item}) + // for open, change and close text document events documents.listen(connection); diff --git a/server/src/wordCompletion.ts b/server/src/wordCompletion.ts index 3738c3b..9d13248 100644 --- a/server/src/wordCompletion.ts +++ b/server/src/wordCompletion.ts @@ -22,6 +22,10 @@ export function selectCompletion(textDocumentPosition : TextDocumentPositionPara return completionCommon().concat(completionImplementation()) } + if(textDocumentPosition.textDocument.uri.endsWith(".def")){ + return completionDefinition() + } + if(textDocumentPosition.textDocument.uri.endsWith(".sys")){ return completionEventB() } @@ -31,13 +35,24 @@ export function selectCompletion(textDocumentPosition : TextDocumentPositionPara } + +function completionDefinition() : CompletionItem []{ + return[ + { + label: 'DEFINITION', + kind: CompletionItemKind.Text, + } + ] + + +} + function completionAbstractMachine() : CompletionItem[] { return [ { label: 'MACHINE', kind: CompletionItemKind.Text, - data: 1 } ] } @@ -46,7 +61,7 @@ function completionImplementation() : CompletionItem[] { return [ { - label: 'IMPLEMENTIATION', + label: 'IMPLEMENTATION', kind: CompletionItemKind.Text, }, { @@ -122,99 +137,1343 @@ function completionCommon() : CompletionItem[] { { label: 'OPERATIONS', kind: CompletionItemKind.Text, - } - ] -} - -function completionCommonAbstract() : CompletionItem[] { - return [ + }, { - label: 'VARIABLES', + label: 'END', kind: CompletionItemKind.Text, }, { - label: 'CONSTANTS', - kind: CompletionItemKind.Text, - } - ] -} - - - -function completionEventB() : CompletionItem[] { - - return [ + label:'skip', + kind:CompletionItemKind.Text, + }, { - label: 'CONTEXT', - kind: CompletionItemKind.Text, + label:'id', + kind:CompletionItemKind.Text, }, { - label: 'EXTENDS', - kind: CompletionItemKind.Text, + label:'closure', + kind:CompletionItemKind.Text, }, { - label: 'SETS', - kind: CompletionItemKind.Text, + label:'closure1', + kind:CompletionItemKind.Text, }, { - label: 'CONSTANTS', - kind: CompletionItemKind.Text, + label:'iterate', + kind:CompletionItemKind.Text, }, { - label: 'AXIOMS', - kind: CompletionItemKind.Text, + label:'pred', + kind:CompletionItemKind.Text, }, { - label: 'END', - kind: CompletionItemKind.Text, + label:'succ', + kind:CompletionItemKind.Text, }, { - label: 'MACHINE', - kind: CompletionItemKind.Text, + label:'prj1', + kind:CompletionItemKind.Text, }, { - label: 'REFINES', - kind: CompletionItemKind.Text, + label:'prj2', + kind:CompletionItemKind.Text, }, { - label: 'SEES', - kind: CompletionItemKind.Text, + label:'ran', + kind:CompletionItemKind.Text, }, { - label: 'VARIABLES', - kind: CompletionItemKind.Text, - } - , + label:'dom', + kind:CompletionItemKind.Text, + }, { - label: 'INVARIANT', - kind: CompletionItemKind.Text, + label:'POW', + kind:CompletionItemKind.Text, }, { - label: 'EVENTS', - kind: CompletionItemKind.Text, + label:'POW1', + kind:CompletionItemKind.Text, }, { - label: 'EVENT', - kind: CompletionItemKind.Text, + label:'NAT', + kind:CompletionItemKind.Text, }, { - label: 'WHERE', - kind: CompletionItemKind.Text, + label:'NAT1', + kind:CompletionItemKind.Text, }, { - label: 'ANY', - kind: CompletionItemKind.Text, + label:'INT', + kind:CompletionItemKind.Text, }, { - label: 'WITH', - kind: CompletionItemKind.Text, + label:'INTEGER', + kind:CompletionItemKind.Text, }, { - label: 'THEN', - kind: CompletionItemKind.Text, + label:'NATURAL', + kind:CompletionItemKind.Text, }, { - label: 'END', + label:'NATURAL1', + kind:CompletionItemKind.Text, + }, + { + label:'MININT', + kind:CompletionItemKind.Text, + }, + { + label:'MAXINT', + kind:CompletionItemKind.Text, + }, + { + label:'STRING', + kind:CompletionItemKind.Text, + }, + { + label:'FIN', + kind:CompletionItemKind.Text, + }, + { + label:'FIN1', + kind:CompletionItemKind.Text, + }, + { + label:'card', + kind:CompletionItemKind.Text, + }, + { + label:'union', + kind:CompletionItemKind.Text, + }, + { + label:'UNION', + kind:CompletionItemKind.Text, + }, + { + label:'inter', + kind:CompletionItemKind.Text, + }, + { + label:'INTER', + kind:CompletionItemKind.Text, + }, + { + label:'PI', + kind:CompletionItemKind.Text, + }, + { + label:'SIGMA', + kind:CompletionItemKind.Text, + }, + { + label:'mod', + kind:CompletionItemKind.Text, + }, + { + label:'seq', + kind:CompletionItemKind.Text, + }, + { + label:'seq1', + kind:CompletionItemKind.Text, + }, + { + label:'iseq', + kind:CompletionItemKind.Text, + }, + { + label:'iseq1', + kind:CompletionItemKind.Text, + }, + { + label:'perm', + kind:CompletionItemKind.Text, + }, + { + label:'size', + kind:CompletionItemKind.Text, + }, + { + label:'rev', + kind:CompletionItemKind.Text, + }, + { + label:'first', + kind:CompletionItemKind.Text, + }, + { + label:'last', + kind:CompletionItemKind.Text, + }, + { + label:'front', + kind:CompletionItemKind.Text, + }, + { + label:'tail', + kind:CompletionItemKind.Text, + }, + { + label:'conc', + kind:CompletionItemKind.Text, + }, + { + label:'max', + kind:CompletionItemKind.Text, + }, + { + label:'min', + kind:CompletionItemKind.Text, + }, + { + label:'or', + kind:CompletionItemKind.Text, + }, + { + label:'not', + kind:CompletionItemKind.Text, + }, + { + label:'bool', + kind:CompletionItemKind.Text, + }, + { + label:'BOOL', + kind:CompletionItemKind.Text, + }, + { + label:'TRUE', + kind:CompletionItemKind.Text, + }, + { + label:'FALSE', + kind:CompletionItemKind.Text, + }, + { + label:'fnc', + kind:CompletionItemKind.Text, + }, + { + label:'rel', + kind:CompletionItemKind.Text, + }, + { + label:'rec', + kind:CompletionItemKind.Text, + }, + { + label:'struct', + kind:CompletionItemKind.Text, + }, + { + label:'left', + kind:CompletionItemKind.Text, + }, + { + label:'right', + kind:CompletionItemKind.Text, + }, + { + label:'tree', + kind:CompletionItemKind.Text, + }, + { + label:'btree', + kind:CompletionItemKind.Text, + }, + { + label:'top', + kind:CompletionItemKind.Text, + }, + { + label:'postfix', + kind:CompletionItemKind.Text, + }, + { + label:'mirror', + kind:CompletionItemKind.Text, + }, + { + label:'prefix', + kind:CompletionItemKind.Text, + }, + { + label:'infix', + kind:CompletionItemKind.Text, + }, + { + label:'sons', + kind:CompletionItemKind.Text, + }, + { + label:'bin', + kind:CompletionItemKind.Text, + }, + { + label:'son', + kind:CompletionItemKind.Text, + }, + { + label:'arity', + kind:CompletionItemKind.Text, + }, + { + label:'subtree', + kind:CompletionItemKind.Text, + }, + { + label:'rank', + kind:CompletionItemKind.Text, + }, + { + label:'father', + kind:CompletionItemKind.Text, + }, + { + label:'const', + kind:CompletionItemKind.Text, + }, + { + label:'sizet', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_ALLOW_LOCAL_OPERATION_CALLS', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_ALLOW_INCOMPLETE_SETUP_CONSTANTS', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_CHR', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_CLPFD', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_COMPRESSION', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_CSE', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_DEFAULT_SETSIZE', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_DOUBLE_EVALUATION', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_EXPAND_FORALL_UPTO', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_INVARIANT_CHECKING', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_KODKOD', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_KODKOD_ONLY_FULL', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_KODKOD_MAX_NR_SOLS', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_KODKOD_SYMMETRY', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_KODKOD_SAT_SOLVER', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_MAXINT', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_MAX_DISPLAY_SET', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_MAX_INITIALISATIONS', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_MAX_OPERATIONS', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_MEMO', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_MININT', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_OPTIMIZE_AST', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_PGE', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_PROOF_INFO', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_RANDOMISE_ENUMERATION_ORDER', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_SMT', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_SMT_SUPPORTED_INTERPRETER', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_STATIC_ORDERING', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_STATIC_SYMMETRY_DETECTION', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_SYMBOLIC', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_SYMMETRY_MODE', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_TIME_OUT', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_TK_CUSTOM_STATE_VIEW_PADDING', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_TK_CUSTOM_STATE_VIEW_STRING_PADDING', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_TRACE_INFO', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_TRY_FIND_ABORT', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_TYPE_CHECK_DEFINITIONS', + kind:CompletionItemKind.Text, + }, + { + label:'SET_PREF_USE_RECORD_CONSTRUCTION', + kind:CompletionItemKind.Text, + }, + { + label:'HEURISTIC_FUNCTION', + kind:CompletionItemKind.Text, + }, + { + label:'CUSTOM_GRAPH_EDGES', + kind:CompletionItemKind.Text, + }, + { + label:'CUSTOM_GRAPH_NODES', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_IMG', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_IMG0', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_IMG1', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_IMG2', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_IMG3', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_IMG4', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_IMG5', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_IMG6', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_IMG7', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_IMG8', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_IMG9', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_FUNCTION_DEFAULT', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_FUNCTION', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_FUNCTION0', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_FUNCTION1', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_FUNCTION2', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_FUNCTION3', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_FUNCTION4', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_FUNCTION5', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_FUNCTION6', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_FUNCTION7', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_FUNCTION8', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_FUNCTION9', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_RIGHT_CLICK', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_CLICK', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_STR_JUSTIFY_LEFT', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_STR_JUSTIFY_RIGHT', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_STR', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_STR1', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_STR2', + kind:CompletionItemKind.Text, + }, + { + label:'ANIMATION_STR3', + kind:CompletionItemKind.Text, + }, + { + label:'CODES_TO_STRING', + kind:CompletionItemKind.Text, + }, + { + label:'GOAL', + kind:CompletionItemKind.Text, + }, + { + label:'SCOPE', + kind:CompletionItemKind.Text, + }, + { + label:'DO_NOT_ENUMERATE', + kind:CompletionItemKind.Text, + }, + { + label:'FORCE', + kind:CompletionItemKind.Text, + }, + { + label:'LEQ_SYM_BREAK', + kind:CompletionItemKind.Text, + }, + { + label:'REPLACE', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_APPEND', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_CONC', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_LENGTH', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_SPLIT', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_JOIN', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_CHARS', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_CODES', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_PADLEFT', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_REV', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_TO_INT', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_TO_LOWER', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_TO_UPPER', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_IS_ALPHANUMERIC', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_IS_DECIMAL', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_IS_INT', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_IS_NUMBER', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_CONTAINS_STRING', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_EQUAL_CASE_INSENSITIVE', + kind:CompletionItemKind.Text, + }, + { + label:'DEC_STRING_TO_INT', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_TO_ENUM', + kind:CompletionItemKind.Text, + }, + { + label:'STRING_IS_NUMBER', + kind:CompletionItemKind.Text, + }, + { + label:'TYPED_STRING_TO_ENUM', + kind:CompletionItemKind.Text, + }, + { + label:'INT_TO_STRING', + kind:CompletionItemKind.Text, + }, + { + label:'INT_TO_DEC_STRING', + kind:CompletionItemKind.Text, + }, + { + label:'INT_TO_HEX_STRING', + kind:CompletionItemKind.Text, + }, + { + label:'STRINGIFY', + kind:CompletionItemKind.Text, + }, + { + label:'TO_STRING', + kind:CompletionItemKind.Text, + }, + { + label:'TO_INT', + kind:CompletionItemKind.Text, + }, + { + label:'FORMAT_TO_STRING', + kind:CompletionItemKind.Text, + }, + { + label:'PRINT', + kind:CompletionItemKind.Text, + }, + { + label:'PRINTF', + kind:CompletionItemKind.Text, + }, + { + label:'FPRINTF', + kind:CompletionItemKind.Text, + }, + { + label:'printf', + kind:CompletionItemKind.Text, + }, + { + label:'vprintf', + kind:CompletionItemKind.Text, + }, + { + label:'fprintf', + kind:CompletionItemKind.Text, + }, + { + label:'observe', + kind:CompletionItemKind.Text, + }, + { + label:'ABS', + kind:CompletionItemKind.Text, + }, + { + label:'CDIV', + kind:CompletionItemKind.Text, + }, + { + label:'FDIV', + kind:CompletionItemKind.Text, + }, + { + label:'GCD', + kind:CompletionItemKind.Text, + }, + { + label:'MSB', + kind:CompletionItemKind.Text, + }, + { + label:'COS', + kind:CompletionItemKind.Text, + }, + { + label:'SIN', + kind:CompletionItemKind.Text, + }, + { + label:'TAN', + kind:CompletionItemKind.Text, + }, + { + label:'SQRT', + kind:CompletionItemKind.Text, + }, + { + label:'BNOT', + kind:CompletionItemKind.Text, + }, + { + label:'BAND', + kind:CompletionItemKind.Text, + }, + { + label:'BOR', + kind:CompletionItemKind.Text, + }, + { + label:'BXOR', + kind:CompletionItemKind.Text, + }, + { + label:'BLSHIFT', + kind:CompletionItemKind.Text, + }, + { + label:'BRSHIFT', + kind:CompletionItemKind.Text, + }, + { + label:'RANDOM', + kind:CompletionItemKind.Text, + }, + { + label:'NORMAL', + kind:CompletionItemKind.Text, + }, + { + label:'random_element', + kind:CompletionItemKind.Text, + }, + { + label:'random_subset', + kind:CompletionItemKind.Text, + }, + { + label:'random_ordering', + kind:CompletionItemKind.Text, + }, + { + label:'random_permutation', + kind:CompletionItemKind.Text, + }, + { + label:'random_numset', + kind:CompletionItemKind.Text, + }, + { + label:'READ_FILE_AS_STRINGS', + kind:CompletionItemKind.Text, + }, + { + label:'READ_LINE', + kind:CompletionItemKind.Text, + }, + { + label:'CHOOSE', + kind:CompletionItemKind.Text, + }, + { + label:'MU', + kind:CompletionItemKind.Text, + }, + { + label:'REGEX_MATCH', + kind:CompletionItemKind.Text, + }, + { + label:'REGEX_REPLACE', + kind:CompletionItemKind.Text, + }, + { + label:'REGEX_SEARCH_STR', + kind:CompletionItemKind.Text, + }, + { + label:'REGEX_SEARCH', + kind:CompletionItemKind.Text, + }, + { + label:'REGEX_SEARCH_ALL', + kind:CompletionItemKind.Text, + }, + { + label:'IS_REGEX', + kind:CompletionItemKind.Text, + }, + { + label:'SORT', + kind:CompletionItemKind.Text, + }, + { + label:'SQUASH', + kind:CompletionItemKind.Text, + }, + { + label:'SUB_STRING', + kind:CompletionItemKind.Text, + }, + { + label:'HASH', + kind:CompletionItemKind.Text, + }, + { + label:'SHA_HASH', + kind:CompletionItemKind.Text, + }, + { + label:'SHA_HASH_HEX', + kind:CompletionItemKind.Text, + }, + { + label:'READ_CSV', + kind:CompletionItemKind.Text, + }, + { + label:'READ_CSV_SEQUENCE', + kind:CompletionItemKind.Text, + }, + { + label:'READ_XML', + kind:CompletionItemKind.Text, + }, + { + label:'READ_XML_FROM_STRING', + kind:CompletionItemKind.Text, + }, + { + label:'WRITE_XML', + kind:CompletionItemKind.Text, + }, + { + label:'WRITE_XML_TO_STRING', + kind:CompletionItemKind.Text, + }, + { + label:'MACHINE', + kind:CompletionItemKind.Text, + }, + { + label:'MODEL', + kind:CompletionItemKind.Text, + }, + { + label:'SYSTEM', + kind:CompletionItemKind.Text, + }, + { + label:'REFINEMENT', + kind:CompletionItemKind.Text, + }, + { + label:'IMPLEMENTATION', + kind:CompletionItemKind.Text, + }, + { + label:'REFINES', + kind:CompletionItemKind.Text, + }, + { + label:'USES', + kind:CompletionItemKind.Text, + }, + { + label:'INCLUDES', + kind:CompletionItemKind.Text, + }, + { + label:'SEES', + kind:CompletionItemKind.Text, + }, + { + label:'IMPORTS', + kind:CompletionItemKind.Text, + }, + { + label:'EXTENDS', + kind:CompletionItemKind.Text, + }, + { + label:'PROMOTES', + kind:CompletionItemKind.Text, + }, + { + label:'SETS', + kind:CompletionItemKind.Text, + }, + { + label:'INITIALISATION', + kind:CompletionItemKind.Text, + }, + { + label:'OPERATIONS', + kind:CompletionItemKind.Text, + }, + { + label:'LOCAL_OPERATIONS', + kind:CompletionItemKind.Text, + }, + { + label:'EVENTS', + kind:CompletionItemKind.Text, + }, + { + label:'THEOREMS', + kind:CompletionItemKind.Text, + }, + { + label:'INVARIANT', + kind:CompletionItemKind.Text, + }, + { + label:'VARIANT', + kind:CompletionItemKind.Text, + }, + { + label:'DEFINITIONS', + kind:CompletionItemKind.Text, + }, + { + label:'ASSERTIONS', + kind:CompletionItemKind.Text, + }, + { + label:'ASSERT', + kind:CompletionItemKind.Text, + }, + { + label:'VARIABLES', + kind:CompletionItemKind.Text, + }, + { + label:'ABSTRACT_VARIABLES', + kind:CompletionItemKind.Text, + }, + { + label:'CONCRETE_VARIABLES', + kind:CompletionItemKind.Text, + }, + { + label:'CONSTANTS', + kind:CompletionItemKind.Text, + }, + { + label:'CONSTRAINTS', + kind:CompletionItemKind.Text, + }, + { + label:'ABSTRACT_CONSTANTS', + kind:CompletionItemKind.Text, + }, + { + label:'CONCRETE_CONSTANTS', + kind:CompletionItemKind.Text, + }, + { + label:'PROPERTIES', + kind:CompletionItemKind.Text, + }, + { + label:'VALUES', + kind:CompletionItemKind.Text, + }, + { + label:'SELECT', + kind:CompletionItemKind.Text, + }, + { + label:'THEN', + kind:CompletionItemKind.Text, + }, + { + label:'END', + kind:CompletionItemKind.Text, + }, + { + label:'IF', + kind:CompletionItemKind.Text, + }, + { + label:'ANY', + kind:CompletionItemKind.Text, + }, + { + label:'WHERE', + kind:CompletionItemKind.Text, + }, + { + label:'WHEN', + kind:CompletionItemKind.Text, + }, + { + label:'ELSE', + kind:CompletionItemKind.Text, + }, + { + label:'ELSIF', + kind:CompletionItemKind.Text, + }, + { + label:'PRE', + kind:CompletionItemKind.Text, + }, + { + label:'BEGIN', + kind:CompletionItemKind.Text, + }, + { + label:'CHOICE', + kind:CompletionItemKind.Text, + }, + { + label:'WHILE', + kind:CompletionItemKind.Text, + }, + { + label:'DO', + kind:CompletionItemKind.Text, + }, + { + label:'VAR', + kind:CompletionItemKind.Text, + }, + { + label:'EITHER', + kind:CompletionItemKind.Text, + }, + { + label:'OR', + kind:CompletionItemKind.Text, + }, + { + label:'LET', + kind:CompletionItemKind.Text, + }, + { + label:'BE', + kind:CompletionItemKind.Text, + }, + { + label:'IN', + kind:CompletionItemKind.Text, + }, + { + label:'CASE', + kind:CompletionItemKind.Text, + }, + { + label:'OF', + kind:CompletionItemKind.Text, + }, + { + label:'ref', + kind:CompletionItemKind.Text, + }, + { + label:'RULES_MACHINE', + kind:CompletionItemKind.Text, + }, + { + label:'RULE_ANY', + kind:CompletionItemKind.Text, + }, + { + label:'RULE_FORALL', + kind:CompletionItemKind.Text, + }, + { + label:'RULEID', + kind:CompletionItemKind.Text, + }, + { + label:'RULE', + kind:CompletionItemKind.Text, + }, + { + label:'COMPUTATION', + kind:CompletionItemKind.Text, + }, + { + label:'DEPENDS_ON_COMPUTATION', + kind:CompletionItemKind.Text, + }, + { + label:'DEPENDS_ON_RULE', + kind:CompletionItemKind.Text, + }, + { + label:'COUNTEREXAMPLE', + kind:CompletionItemKind.Text, + }, + { + label:'EXPECT', + kind:CompletionItemKind.Text, + }, + { + label:'ERROR_TYPE', + kind:CompletionItemKind.Text, + }, + { + label:'ERROR_TYPES', + kind:CompletionItemKind.Text, + }, + { + label:'BODY', + kind:CompletionItemKind.Text, + }, + { + label:'REFERENCES', + kind:CompletionItemKind.Text, + }, + { + label:'SUCCEEDED_RULE', + kind:CompletionItemKind.Text, + }, + { + label:'FAILED_RULE', + kind:CompletionItemKind.Text, + }, + { + label:'GET_RULE_COUNTEREXAMPLES', + kind:CompletionItemKind.Text, + }, + { + label:'FUNCTION', + kind:CompletionItemKind.Text, + }, + { + label:'PRECONDITION', + kind:CompletionItemKind.Text, + }, + { + label:'DEFINE', + kind:CompletionItemKind.Text, + }, + { + label:'TYPE', + kind:CompletionItemKind.Text, + }, + { + label:'VALUE', + kind:CompletionItemKind.Text, + }, + + ] +} + +function completionCommonAbstract() : CompletionItem[] { + return [ + { + label: 'VARIABLES', + kind: CompletionItemKind.Text, + }, + { + label: 'CONSTANTS', + kind: CompletionItemKind.Text, + } + ] +} + + + +function completionEventB() : CompletionItem[] { + + return [ + { + label: 'CONTEXT', + kind: CompletionItemKind.Text, + }, + { + label: 'EXTENDS', + kind: CompletionItemKind.Text, + }, + { + label: 'SETS', + kind: CompletionItemKind.Text, + }, + { + label: 'CONSTANTS', + kind: CompletionItemKind.Text, + }, + { + label: 'AXIOMS', + kind: CompletionItemKind.Text, + }, + { + label: 'END', + kind: CompletionItemKind.Text, + }, + { + label: 'MACHINE', + kind: CompletionItemKind.Text, + }, + { + label: 'REFINES', + kind: CompletionItemKind.Text, + }, + { + label: 'SEES', + kind: CompletionItemKind.Text, + }, + { + label: 'VARIABLES', + kind: CompletionItemKind.Text, + }, + { + label: 'INVARIANT', + kind: CompletionItemKind.Text, + }, + { + label: 'EVENTS', + kind: CompletionItemKind.Text, + }, + { + label: 'Event', + kind: CompletionItemKind.Text, + }, + { + label: 'Initialisation', + kind: CompletionItemKind.Text, + }, + { + label: 'where', + kind: CompletionItemKind.Text, + }, + { + label: 'any', + kind: CompletionItemKind.Text, + }, + { + label: 'with', + kind: CompletionItemKind.Text, + }, + { + label: 'then', kind: CompletionItemKind.Text, } ] -- GitLab