diff --git a/server/src/server.ts b/server/src/server.ts
index ef3dee3ed718fb7878e733aa325b1897ea4eab29..6d316f6acb12149b6e36cb25dc8f3028dbb17792 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 3738c3bf9801f78b6b8a90347bfc6f8e50704211..9d13248827868ffcb4e1d3e9d5aecd8c743f5563 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,
 		}
 	]