From cd83bbc36387cca3a5194ec596bdbc046cc1adec Mon Sep 17 00:00:00 2001
From: SeeBasTStick <sebastian.stock@hhu.de>
Date: Tue, 19 May 2020 14:09:25 +0200
Subject: [PATCH] added word completion, removed unued server features
---
README.md | 1 +
server/src/server.ts | 80 +------------
server/src/wordCompletion.ts | 221 +++++++++++++++++++++++++++++++++++
3 files changed, 225 insertions(+), 77 deletions(-)
create mode 100644 server/src/wordCompletion.ts
diff --git a/README.md b/README.md
index d621c95..8c5aad8 100644
--- a/README.md
+++ b/README.md
@@ -27,6 +27,7 @@ This extension contributes the following settings:
## Future plans
- Linter Support
- Keyword support
+- Quickfix support
## Release Notes
diff --git a/server/src/server.ts b/server/src/server.ts
index 670148b..ef3dee3 100644
--- a/server/src/server.ts
+++ b/server/src/server.ts
@@ -15,9 +15,6 @@ import {
TextDocumentPositionParams,
TextDocumentSyncKind,
InitializeResult,
- NotificationType0,
- PublishDiagnosticsNotification
-
} from 'vscode-languageserver';
import {
@@ -27,9 +24,11 @@ import {
import { URI } from 'vscode-uri';
import * as fs from 'fs';
import {ErrorMatcher} from './ErrorMatcher';
+import * as wordComplition from './wordCompletion'
import * as path from 'path';
+
// Create a connection for the server. The connection uses Node's IPC as a transport.
// Also include all preview / proposed LSP features.
let connection = createConnection(ProposedFeatures.all);
@@ -143,11 +142,6 @@ documents.onDidSave(change => {
validateTextDocument(change.document)
})
-// The content of a text document has changed. This event is emitted
-// when the text document first opened or when its content has changed.
-documents.onDidChangeContent(change => {
-// validateTextDocument(change.document);
-});
async function validateTextDocument(textDocument: TextDocument): Promise<void> {
let settings = await getDocumentSettings(textDocument.uri);
@@ -189,8 +183,6 @@ async function validateTextDocument(textDocument: TextDocument): Promise<void> {
});
}
-
-
}
function correctPath(path:string): boolean{
@@ -203,81 +195,15 @@ function correctPath(path:string): boolean{
return true
}
-connection.onDidChangeWatchedFiles(_change => {
- // Monitored files have change in VSCode
- connection.console.log('We received an file change event');
-});
-
-
// This handler provides the initial list of the completion items.
connection.onCompletion(
-
(textDocumentPosition: TextDocumentPositionParams): CompletionItem[] => {
-
- return [
- {
- label: 'MACHINE',
- kind: CompletionItemKind.Text,
- data: 1
- },
-
- {
- label: 'VARIABLES',
- kind: CompletionItemKind.Text,
- data: 2
- },
- {
- label: 'CONSTANTS',
- kind: CompletionItemKind.Text,
- data: 3
- },
- {
- label: 'OPERATIONS',
- kind: CompletionItemKind.Text,
- data: 4
- },
-
- ];
- }
-);
-
-// This handler resolves additional information for the item selected in
-// the completion list.
-connection.onCompletionResolve(
- (item: CompletionItem): CompletionItem => {
- if (item.data === 1) {
- item.detail = 'TypeScript details';
- item.documentation = 'TypeScript documentation';
- } else if (item.data === 2) {
- item.detail = 'JavaScript details';
- item.documentation = 'JavaScript documentation';
- }
- return item;
+ return wordComplition.selectCompletion(textDocumentPosition)
}
);
-/*
-connection.onDidOpenTextDocument((params) => {
- // A text document got opened in VSCode.
- // params.textDocument.uri uniquely identifies the document. For documents store on disk this is a file URI.
- // params.textDocument.text the initial full content of the document.
- connection.console.log(`${params.textDocument.uri} opened.`);
-});
-connection.onDidChangeTextDocument((params) => {
- // The content of a text document did change in VSCode.
- // params.textDocument.uri uniquely identifies the document.
- // params.contentChanges describe the content changes to the document.
- connection.console.log(`${params.textDocument.uri} changed: ${JSON.stringify(params.contentChanges)}`);
-});
-connection.onDidCloseTextDocument((params) => {
- // A text document got closed in VSCode.
- // params.textDocument.uri uniquely identifies the document.
- connection.console.log(`${params.textDocument.uri} closed.`);
-});
-*/
-// Make the text document manager listen on the connection
// for open, change and close text document events
documents.listen(connection);
diff --git a/server/src/wordCompletion.ts b/server/src/wordCompletion.ts
new file mode 100644
index 0000000..3738c3b
--- /dev/null
+++ b/server/src/wordCompletion.ts
@@ -0,0 +1,221 @@
+
+import {
+
+ CompletionItem,
+ CompletionItemKind,
+ TextDocumentPositionParams,
+
+} from 'vscode-languageserver';
+
+export function selectCompletion(textDocumentPosition : TextDocumentPositionParams) : CompletionItem[]{
+
+
+ if(textDocumentPosition.textDocument.uri.endsWith(".mch")){
+ return completionCommon().concat(completionAbstractMachine()).concat(completionCommonAbstract())
+ }
+
+ if(textDocumentPosition.textDocument.uri.endsWith(".ref")){
+ return completionCommon().concat(completionRefinement()).concat(completionCommonAbstract())
+ }
+
+ if(textDocumentPosition.textDocument.uri.endsWith(".imp")){
+ return completionCommon().concat(completionImplementation())
+ }
+
+ if(textDocumentPosition.textDocument.uri.endsWith(".sys")){
+ return completionEventB()
+ }
+
+ return []
+
+}
+
+
+function completionAbstractMachine() : CompletionItem[] {
+
+ return [
+ {
+ label: 'MACHINE',
+ kind: CompletionItemKind.Text,
+ data: 1
+ }
+ ]
+}
+
+function completionImplementation() : CompletionItem[] {
+
+ return [
+ {
+ label: 'IMPLEMENTIATION',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'IMPORTS',
+ kind: CompletionItemKind.Text,
+ }
+ ]
+}
+
+
+function completionRefinement() : CompletionItem[] {
+
+ return [
+ {
+ label: 'REFINEMENT',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'REFINES',
+ kind: CompletionItemKind.Text,
+ },
+
+ ]
+}
+
+function completionCommon() : CompletionItem[] {
+
+ return [
+ {
+ label: 'SEES',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'INCLUDES',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'PROMOTES',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'EXTENDS',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'SETS',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'CONCRETE_CONSTANTS',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'PROPERTIES',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'CONCRETE_VARIALBES',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'INVARIANT',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'ASSERTIONS',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'INITIALIZATION',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'OPERATIONS',
+ 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: 'WHERE',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'ANY',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'WITH',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'THEN',
+ kind: CompletionItemKind.Text,
+ },
+ {
+ label: 'END',
+ kind: CompletionItemKind.Text,
+ }
+ ]
+}
\ No newline at end of file
--
GitLab