diff --git a/README.md b/README.md index d621c955adc93d561233186131b3011102bc091a..8c5aad855d392ca755077d463a773fd69c5d097e 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 670148b7396898e801a96873ab6fc2d8bf2234a6..ef3dee3ed718fb7878e733aa325b1897ea4eab29 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 0000000000000000000000000000000000000000..3738c3bf9801f78b6b8a90347bfc6f8e50704211 --- /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