diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index d11d34066..64be7cdde 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -4,11 +4,11 @@ on: push: workflow_dispatch: jobs: - build: + build_lambdapi: strategy: fail-fast: false matrix: - ocaml-version: [5.1.0, 5.0.0, 4.14.1, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1] + ocaml-version: [5.1.1, 5.0.0, 4.14.1, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1] runs-on: ubuntu-latest steps: - name: checking out lambdapi repo ... @@ -34,8 +34,15 @@ jobs: eval $(opam env) #why3 config detect make tests + build_vscode_extension: + strategy: + fail-fast: false + runs-on: ubuntu-latest + steps: + - name: checking out lambdapi repo ... + uses: actions/checkout@v4 - name: Use Node.js - uses: actions/setup-node@v3 + uses: actions/setup-node@v4 with: node-version: latest - name: generate-vscode-extension @@ -44,7 +51,7 @@ jobs: npm install -g vsce make build-vscode-extension - name: publish vscode extension - uses: actions/upload-artifact@v2 + uses: actions/upload-artifact@v4 with: name: assets-for-download path: editors/vscode/extensionFolder diff --git a/editors/vscode/CHANGES.md b/editors/vscode/CHANGES.md index df4bbcf1d..fdecc2e40 100644 --- a/editors/vscode/CHANGES.md +++ b/editors/vscode/CHANGES.md @@ -4,6 +4,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/), and this project adheres to [Semantic Versioning](https://semver.org/). ## [Unreleased] +- code refactoring of the client for maintenability. +- fix the bug that causes the proof navigation to malfunction when the Goals panel is closed by the user. Now the panel is recreated whenever needed. ## [0.1.2] - 2020-12-10 - use vscode configuration for lambdapi.path to call the lambdapi LSP server diff --git a/editors/vscode/package-lock.json b/editors/vscode/package-lock.json index 43ae65531..0ccdde9ae 100644 --- a/editors/vscode/package-lock.json +++ b/editors/vscode/package-lock.json @@ -19,7 +19,7 @@ "typescript": "^5.2.2" }, "engines": { - "vscode": "^1.37.0" + "vscode": "^1.82.0" } }, "node_modules/@types/mocha": { diff --git a/editors/vscode/package.json b/editors/vscode/package.json index 557c48cb4..fc13a67c5 100644 --- a/editors/vscode/package.json +++ b/editors/vscode/package.json @@ -153,7 +153,7 @@ } ] }, - "main": "out/src/client.js", + "main": "out/src/browser.js", "scripts": { "vscode:prepublish": "npm run compile", "compile": "tsc -p ./", diff --git a/editors/vscode/src/browser.ts b/editors/vscode/src/browser.ts new file mode 100644 index 000000000..30b764b7b --- /dev/null +++ b/editors/vscode/src/browser.ts @@ -0,0 +1,22 @@ +import { ExtensionContext, window } from "vscode"; +import { LanguageClient } from "vscode-languageclient/node"; +import { activateClientLSP, ClientFactoryType, deactivateClientLSP } from "./client"; + +export function activate(context: ExtensionContext): void { + const cf: ClientFactoryType = (context, clientOptions, wsConfig, lspServerPath) => { + let serverOptions = { + command: lspServerPath, + args: ['lsp'] + }; + return new LanguageClient( + "lambdapi", + "lambdapi language server", + serverOptions, + clientOptions); + }; + activateClientLSP(context, cf); +} + +export function deactivate() { + deactivateClientLSP(); +} diff --git a/editors/vscode/src/client.ts b/editors/vscode/src/client.ts index b75427422..7ee27277e 100644 --- a/editors/vscode/src/client.ts +++ b/editors/vscode/src/client.ts @@ -1,39 +1,52 @@ // VSCode extension for https://github.com/Deducteam/lambdapi // a proof assistant based on the λΠ-calculus modulo rewriting -import { - workspace, - ExtensionContext, - Position, - Uri, - commands, - window, - WebviewPanel, - ViewColumn, - TextEditor, - TextDocument, - SnippetString, - Range, - TextEditorDecorationType, - Pseudoterminal, - EventEmitter, - TreeItemCollapsibleState, - WebviewViewProvider, - CancellationToken, - WebviewView, - WebviewViewResolveContext, - TextDocumentChangeEvent, - Diagnostic, - languages +import { + workspace, + ExtensionContext, + Position, + Uri, + commands, + window, + WebviewPanel, + ViewColumn, + TextEditor, + TextDocument, + SnippetString, + Range, + TextEditorDecorationType, + Pseudoterminal, + EventEmitter, + TreeItemCollapsibleState, + WebviewViewProvider, + CancellationToken, + WebviewView, + WebviewViewResolveContext, + TextDocumentChangeEvent, + Diagnostic, + languages, + WorkspaceConfiguration } from 'vscode'; // Insiders API, disabled // import { WebviewEditorInset } from 'vscode'; import { - LanguageClient, + LspClientConfig, + LspServerConfig, + LSPDocumentSelector, +} from "./config"; + +import { + BaseLanguageClient, LanguageClientOptions, RequestType, + RevealOutputChannelOn, + VersionedTextDocumentIdentifier, +} from "vscode-languageclient"; + +import { + LanguageClient, NotificationType, TextDocumentIdentifier, RegistrationRequest, @@ -42,25 +55,247 @@ import { import { assert, time } from 'console'; -let client: LanguageClient; +let client: BaseLanguageClient; + +// Client Factory types +export type ClientFactoryType = ( + context: ExtensionContext, + clientOptions: LanguageClientOptions, + wsConfig: WorkspaceConfiguration, + lspServerPath: any, +) => BaseLanguageClient; + +// The implementation of the VSCode lambdapi extension commands. +function goToProofState(context: ExtensionContext) { -export function activate(context: ExtensionContext) { + const proofState: Position | undefined = context.workspaceState.get('proofState'); + if (!proofState) { + console.log("goToProofState : proofState workspace variable not set properly"); + return; + } + + commands.executeCommand('revealLine', { lineNumber: proofState.line, at: 'center' }); +} + +function toggleCursorMode(context: ExtensionContext): boolean { + let cursorMode: boolean = context.workspaceState.get('cursorMode') ?? false; + + cursorMode = !cursorMode; + context.workspaceState.update('cursorMode', cursorMode); + + if (cursorMode) { + + window.showInformationMessage("Cursor navigation enabled"); + + //By default, follow mode is disabled in cursor mode (because it may be nausea-inducing) + if (context.workspaceState.get('follow')) + toggleFollowMode(context); + } + + else { + + window.showInformationMessage("Cursor navigation disabled"); + + //By default, follow mode is enabled when cursor mode is off (because it is more practical) + if (!context.workspaceState.get('follow')) + toggleFollowMode(context); + } - workspace.onDidChangeTextDocument((e)=>{ + return cursorMode; +} + +function toggleFollowMode(context: ExtensionContext): boolean { + let follow: boolean = context.workspaceState.get('follow') ?? false; + + follow = !follow; + context.workspaceState.update('follow', follow); + + + if (follow) + window.showInformationMessage("Window follows highlights"); + + else + window.showInformationMessage("Window doesn't follow highlights"); + + return follow; +} + +function checkProofForward(context: ExtensionContext) { + + //Checking workspace + const openEditor: TextEditor | undefined = window.activeTextEditor; + if (!openEditor) + return; + + const proofState: Position | undefined = context.workspaceState.get('proofState'); + let panel: WebviewPanel | undefined | null = context.workspaceState.get('panel'); + + if (!proofState) { + console.log('checkProofForward : Workspace variables are not properly defined'); + return; + } + + let newPos = stepCommand(openEditor.document, proofState, true); + if (newPos) + lpRefresh(context, newPos, panel, openEditor); +} + +function checkProofBackward(context: ExtensionContext) { + + //Checking workspace + const openEditor: TextEditor | undefined = window.activeTextEditor; + if (!openEditor) + return; + + const proofState: Position | undefined = context.workspaceState.get('proofState'); + const panel: WebviewPanel | undefined | null = context.workspaceState.get('panel'); + if (!proofState) { + console.log('checkProofBackward : Workspace variables are not properly defined'); + return; + } + + let newPos = stepCommand(openEditor.document, proofState, false); + + //Case the end has not been reached + if (newPos) + lpRefresh(context, newPos, panel, openEditor); +} + +function checkProofUntilCursor(context: ExtensionContext) { + + //Checking workspace + const openEditor: TextEditor | undefined = window.activeTextEditor; + if (!openEditor) + return; + + const proofState: Position | undefined = context.workspaceState.get('proofState'); + const panel: WebviewPanel | undefined | null = context.workspaceState.get('panel'); + + if (!proofState) { + console.log('checkProofUntilCursor : workspace variables are not properly defined'); + return; + } + + //The current position of the cursor + let cursorPosition: Position = openEditor.selection.active; + if (proofState.line == cursorPosition.line) + return; + + //To simplify the code, proof states are always at the beggining of the highlighted line + //So must be the cursor position since it is the new proof state + if (cursorPosition.character != 0) + cursorPosition = new Position(cursorPosition.line, 0); + + context.workspaceState.update('proofState', cursorPosition); //proof state is set to the cursor position + + refreshGoals(panel, openEditor, cursorPosition, context); //Goals panel is refreshed + + highlight(context, cursorPosition, openEditor); +} + +function goToNextProof(context: ExtensionContext) { + nextProof(context, true); +} + +function goToPreviousProof(context: ExtensionContext) { + nextProof(context, false); +} + +function nextProof(context: ExtensionContext, direction: boolean) { + + //Checking workspace + const openEditor: TextEditor | undefined = window.activeTextEditor; + if (!openEditor) { + console.log("No editor opened"); + return; + } + + const proofState: Position | undefined = context.workspaceState.get('proofState'); + const panel: WebviewPanel | undefined | null = context.workspaceState.get('panel'); + + if (!proofState) { + console.log('nextProof : workspace variables are not properly defined'); + return; + } + + //The position of the next proof + let nextProofPos: Position = stepCommand(openEditor.document, proofState, direction, ['begin']); + + context.workspaceState.update('proofState', nextProofPos); //proof state is set to the position of the next proof keyword + + refreshGoals(panel, openEditor, nextProofPos, context); //Goals panel is refreshed + + highlight(context, nextProofPos, openEditor); +} + +// Associate the command command to function fn defined above +function registerCommand(command: string, context: ExtensionContext, fn: (context: ExtensionContext) => void) { + let disposable = commands.registerCommand(command, () => fn(context)); + context.subscriptions.push(disposable); +} + +// This function is called by VSCode when the extension is activated +export function activateClientLSP(context: ExtensionContext, + clientFactory: ClientFactoryType) { + + workspace.onDidChangeTextDocument((e) => { lpDocChangeHandler(e, context); }) + // Please refer to package.json section keybindings, to see the key binding corresponding to the following commands + + /*Toggle cursor mode (defaults to false) + *if true, the "Proof" panel is updated when the cursor is moved + *if false, updated when keybindings are pressed + */ + registerCommand('extension.lambdapi.cursor', context, toggleCursorMode); + //Navigate proof : step forward in a proof + registerCommand('extension.lambdapi.fw', context, checkProofForward); + //Navigate proof : step backward in a proof + registerCommand('extension.lambdapi.bw', context, checkProofBackward); + //Navigate proof : move proof highlight to cursor + registerCommand('extension.lambdapi.tc', context, checkProofUntilCursor); + //Window follows proof or not + registerCommand('extension.lambdapi.reveal', context, toggleFollowMode); + //Center window on proof state + registerCommand('extension.lambdapi.center', context, goToProofState); + //Go to next/previous proof + registerCommand('extension.lambdapi.nx', context, goToNextProof); + registerCommand('extension.lambdapi.pv', context, goToPreviousProof); + + window.onDidChangeActiveTextEditor(e => { + + const proofState: Position | undefined = context.workspaceState.get('proofState'); + const panel: WebviewPanel | undefined | null = context.workspaceState.get('panel'); + + if (!proofState || !panel) { + console.log('onDidChangeActiveTextEditor : workspace variables are not properly defined'); + return; + } + + refreshGoals(panel, e, proofState, context); + }); + + window.onDidChangeTextEditorSelection(e => { + + const cursorMode: boolean = context.workspaceState.get('cursorMode') ?? false; + if (!cursorMode) + return; + + checkProofUntilCursor(context); + }); + //___Declaration of workspace variables___ //Position of the proof cursor : colored highlights show until which point the proof was surveyed - let proofState : Position = new Position(0, 0); + let proofState: Position = new Position(0, 0); context.workspaceState.update('proofState', proofState); //Cursor mode (proof cursor is the regular cursor) activated or not context.workspaceState.update('cursorMode', false); //The range of text to highlight - let range : Range = new Range(new Position(0, 0), proofState); + let range: Range = new Range(new Position(0, 0), proofState); context.workspaceState.update('range', range); //The highlight parameters @@ -72,7 +307,7 @@ export function activate(context: ExtensionContext) { backgroundColor: '#08883555' //highlight color for a dark theme }, rangeBehavior: 1 // ClosedClosed - }); + }); const errorDecoration = window.createTextEditorDecorationType({ light: { backgroundColor: '#FF000055' //highlight color for a light theme @@ -81,133 +316,109 @@ export function activate(context: ExtensionContext) { backgroundColor: '#FF000055' //highlight color for a dark theme }, rangeBehavior: 1 // ClosedClosed - }); + }); context.workspaceState.update('proofDecoration', proofDecoration); context.workspaceState.update('errorDecoration', errorDecoration); //Following mode : whether the window follows proofState automatically or not context.workspaceState.update('follow', true); - + const lspServerPath = workspace.getConfiguration('lambdapi').path; console.log(lspServerPath); - let serverOptions = { - command: lspServerPath, - args: [ 'lsp' ] - // args: [ '--std' ] + const wsConfig = workspace.getConfiguration("lambdapi"); + + let client_version = context.extension.packageJSON.version; + const initializationOptions = LspServerConfig.create( + client_version, + wsConfig + ); + const clientOptions: LanguageClientOptions = { + documentSelector: [ + { scheme: 'file', language: 'lp' }, + { scheme: "file", language: "markdown", pattern: "**/*.lp" }, + ], + outputChannelName: "Lambdapi LSP Server Events", + revealOutputChannelOn: RevealOutputChannelOn.Info, + initializationOptions, + markdown: { isTrusted: true, supportHtml: true }, }; - let clientOptions: LanguageClientOptions = { - documentSelector: [{ scheme: 'file', language: 'lp' }], - }; + // This function starts the client and the server + const start = () => { - const restart = () => { - - if (client) { - client.stop(); - } - - client = new LanguageClient( - 'lambdapi', - 'lambdapi language server', - serverOptions, - clientOptions - ); - - client.start().then( () => { + let cP = new Promise((resolve) => { + // Create a client using the factory + client = clientFactory(context, clientOptions, wsConfig, lspServerPath); + resolve(client); + }); + cP.then((client) => client.start().then(() => { // Create and show panel for proof goals - const panel = window.createWebviewPanel( - 'goals', - 'Goals', - ViewColumn.Two, - {} - ); - context.workspaceState.update('panel', panel); - - window.onDidChangeActiveTextEditor(e => { - - const proofState : Position | undefined = context.workspaceState.get('proofState'); - const panel : WebviewPanel | undefined = context.workspaceState.get('panel'); - - if (!proofState || !panel) { - console.log('onDidChangeActiveTextEditor : workspace variables are not properly defined'); - return; - } + createInfoPanel(context); + }) + ) - refreshGoals(panel, e, proofState, context); - }); - - window.onDidChangeTextEditorSelection(e => { - - const cursorMode : boolean = context.workspaceState.get('cursorMode') ?? false; - if(!cursorMode) - return; - - checkProofUntilCursor(context); - }); + }; - /*Toggle cursor mode (defaults to false) - *if true, the "Proof" panel is updated when the cursor is moved - *if false, updated when keybindings are pressed - */ - commands.registerCommand('extension.lambdapi.cursor', () => toggleCursorMode(context)); - - //Navigate proof : step forward in a proof - commands.registerCommand('extension.lambdapi.fw', () => checkProofForward(context)); - - //Navigate proof : step backward in a proof - commands.registerCommand('extension.lambdapi.bw', () => checkProofBackward(context)); + const stop = () => { } - //Navigate proof : move proof highlight to cursor - commands.registerCommand('extension.lambdapi.tc', () => checkProofUntilCursor(context)); - - //Window follows proof or not - commands.registerCommand('extension.lambdapi.reveal', () => toggleFollowMode(context)) + const restart = () => { + // If the client is running then stop it before starting it again + if (client) { + client.stop(); + } - //Center window on proof state - commands.registerCommand('extension.lambdapi.center', () => goToProofState(context)); + start(); - //Go to next/previous proof - commands.registerCommand('extension.lambdapi.nx', () => nextProof(context, true)); - commands.registerCommand('extension.lambdapi.pv', () => nextProof(context, false)); + }; + // associate the VSCode command "Lambdapi: restart the Lambdapi VSCode mode" with the restart function + registerCommand('extension.lambdapi.restart', context, restart); - }); + start(); +} - context.subscriptions.push(client); - }; - - commands.registerCommand('extension.lambdapi.restart', restart); - - restart(); +//This function creates the Goals panel when proofs are navigated +function createInfoPanel(context: ExtensionContext) { + let panel: WebviewPanel | null = window.createWebviewPanel( + 'goals', + 'Goals', + { preserveFocus: true, viewColumn: ViewColumn.Two }, + {} + ); + // When the panel is closed for some reason, put null to reopen it when the user naviagate proofs again + panel.onDidDispose(() => { + context.workspaceState.update('panel', null); + }); + context.workspaceState.update('panel', panel); } -function lpDocChangeHandler(event : TextDocumentChangeEvent, context: ExtensionContext) { +function lpDocChangeHandler(event: TextDocumentChangeEvent, context: ExtensionContext) { - if(event.document != window.activeTextEditor?.document){ + if (event.document != window.activeTextEditor?.document) { // should not happen console.log("Changes not on the active TextEditor"); return; } - let proofPos : Position | undefined = context.workspaceState.get('proofState'); + let proofPos: Position | undefined = context.workspaceState.get('proofState'); if (!proofPos) proofPos = new Position(0, 0); - let firstChange : Position | undefined = undefined; - for(let i = 0; i < event.contentChanges.length; i++){ + let firstChange: Position | undefined = undefined; + for (let i = 0; i < event.contentChanges.length; i++) { let change = event.contentChanges[i]; - let changeStart : Position = change.range.start; - if(firstChange != undefined) + let changeStart: Position = change.range.start; + if (firstChange != undefined) firstChange = changeStart.isBefore(firstChange) ? changeStart : firstChange; - else + else firstChange = changeStart; } - if(firstChange && firstChange.isBefore(proofPos)){ + if (firstChange && firstChange.isBefore(proofPos)) { // region inside proved region is changed // update the proofState let newPos = stepCommand(event.document, firstChange, false); - const panel : WebviewPanel | undefined = context.workspaceState.get('panel'); + const panel: WebviewPanel | undefined | null = context.workspaceState.get('panel'); if (!panel) { console.log('lpDocChangeHandler : workspace variables are not properly defined'); return; @@ -218,57 +429,57 @@ function lpDocChangeHandler(event : TextDocumentChangeEvent, context: ExtensionC } } -function getFirstError(uri : Uri, before? : Position){ - let diags : Diagnostic[] = languages.getDiagnostics(uri); - let firstError : Position | undefined = undefined; +function getFirstError(uri: Uri, before?: Position) { + let diags: Diagnostic[] = languages.getDiagnostics(uri); + let firstError: Position | undefined = undefined; let ind = 0; - for (let diag of diags){ + for (let diag of diags) { if (diag.severity == 0) {//check if error - if(firstError){ + if (firstError) { firstError = diag.range.start.isBefore(firstError) ? diag.range.start : firstError; } else { firstError = diag.range.start; } } } - if(before){ - if(firstError && firstError.isBefore(before)) return firstError; + if (before) { + if (firstError && firstError.isBefore(before)) return firstError; else return undefined; - } else { + } else { return firstError; } } -function highlight(context : ExtensionContext, newProofState : Position, openEditor : TextEditor) { +function highlight(context: ExtensionContext, newProofState: Position, openEditor: TextEditor) { //Highlighting text - const proofDecoration : TextEditorDecorationType | undefined = context.workspaceState.get('proofDecoration'); - const errorDecoration : TextEditorDecorationType | undefined = context.workspaceState.get('errorDecoration'); + const proofDecoration: TextEditorDecorationType | undefined = context.workspaceState.get('proofDecoration'); + const errorDecoration: TextEditorDecorationType | undefined = context.workspaceState.get('errorDecoration'); const firstError = getFirstError(openEditor.document.uri, newProofState); const zeroPos = new Position(0, 0); - if(!proofDecoration || !errorDecoration) + if (!proofDecoration || !errorDecoration) console.log('Highlights/decorations are not properly defined'); - else{ - if(firstError){ + else { + if (firstError) { decorate(openEditor, new Range(zeroPos, firstError), proofDecoration); decorate(openEditor, new Range(firstError, newProofState), errorDecoration); } else { decorate(openEditor, null, errorDecoration); decorate(openEditor, new Range(zeroPos, newProofState), proofDecoration); } - + } //Scroll until last highlight (if follow mode is toggled) const follow: boolean | undefined = context.workspaceState.get('follow'); - if(follow) - commands.executeCommand('revealLine', {lineNumber: newProofState.line, at: 'center'}); + if (follow) + commands.executeCommand('revealLine', { lineNumber: newProofState.line, at: 'center' }); } -function lpRefresh(context : ExtensionContext, proofPos : Position, panel : WebviewPanel, openEditor : TextEditor) { +function lpRefresh(context: ExtensionContext, proofPos: Position, panel: WebviewPanel | null | undefined, openEditor: TextEditor) { context.workspaceState.update('proofState', proofPos); @@ -277,110 +488,29 @@ function lpRefresh(context : ExtensionContext, proofPos : Position, panel : Webv highlight(context, proofPos, openEditor); } -function nextProof(context : ExtensionContext, direction : boolean) { - - //Checking workspace - const openEditor : TextEditor | undefined = window.activeTextEditor; - if(!openEditor) { - console.log("No editor opened"); - return; - } - - const proofState : Position | undefined = context.workspaceState.get('proofState'); - const panel : WebviewPanel | undefined = context.workspaceState.get('panel'); - - if (!proofState || !panel) { - console.log('nextProof : workspace variables are not properly defined'); - return; - } - - //The position of the next proof - let nextProofPos : Position = stepCommand(openEditor.document, proofState, direction, ['begin']); - - context.workspaceState.update('proofState', nextProofPos); //proof state is set to the position of the next proof keyword - - refreshGoals(panel, openEditor, nextProofPos, context); //Goals panel is refreshed - - highlight(context, nextProofPos, openEditor); -} - -function goToProofState(context : ExtensionContext){ - - const proofState : Position | undefined = context.workspaceState.get('proofState'); - if(!proofState) { - console.log("goToProofState : proofState workspace variable not set properly"); - return; - } - - commands.executeCommand('revealLine', {lineNumber: proofState.line, at: 'center'}); -} - -function toggleCursorMode(context : ExtensionContext) : boolean { - let cursorMode : boolean = context.workspaceState.get('cursorMode') ?? false; - - cursorMode = !cursorMode; - context.workspaceState.update('cursorMode', cursorMode); - - if(cursorMode) { - - window.showInformationMessage("Cursor navigation enabled"); - - //By default, follow mode is disabled in cursor mode (because it may be nausea-inducing) - if( context.workspaceState.get('follow') ) - toggleFollowMode(context); - } - - else { - - window.showInformationMessage("Cursor navigation disabled"); - - //By default, follow mode is enabled when cursor mode is off (because it is more practical) - if( !context.workspaceState.get('follow') ) - toggleFollowMode(context); - } - - return cursorMode; -} - -function toggleFollowMode(context : ExtensionContext) : boolean { - let follow : boolean = context.workspaceState.get('follow') ?? false; - - follow = !follow; - context.workspaceState.update('follow', follow); - - - if(follow) - window.showInformationMessage("Window follows highlights"); - - else - window.showInformationMessage("Window doesn't follow highlights"); - - return follow; -} - -function decorate(openEditor : TextEditor, range : Range | null, decorationType : TextEditorDecorationType) { - if(range) +function decorate(openEditor: TextEditor, range: Range | null, decorationType: TextEditorDecorationType) { + if (range) openEditor.setDecorations(decorationType, [range]); else openEditor.setDecorations(decorationType, []); } // returns the Position of next or previous command -function stepCommand(document: TextDocument, currentPos: Position, forward: boolean, terminators?: string[]){ +function stepCommand(document: TextDocument, currentPos: Position, forward: boolean, terminators?: string[]) { - if(terminators === undefined || terminators === null) + if (terminators === undefined || terminators === null) terminators = [';', 'begin', '{']; - let docBegin : Position = document.positionAt(0); - let docEnd : Position = new Position(document.lineCount, 0); + let docBegin: Position = document.positionAt(0); + let docEnd: Position = new Position(document.lineCount, 0); - const minPos = (a : Position, b : Position) => a.compareTo(b) < 0 ? a : b; - const maxPos = (a : Position, b : Position) => a.compareTo(b) > 0 ? a : b; + const minPos = (a: Position, b: Position) => a.compareTo(b) < 0 ? a : b; + const maxPos = (a: Position, b: Position) => a.compareTo(b) > 0 ? a : b; const termRegex = new RegExp(terminators.join("|"), 'gi'); let termPositions = [...document.getText().matchAll(termRegex)] .map(rm => rm.index ? rm.index + rm[0].length : undefined) - .filter((x) : x is number => x !== undefined) // remove undefined + .filter((x): x is number => x !== undefined) // remove undefined .map(x => document.positionAt(x)); let nextCmdPos = termPositions @@ -390,137 +520,75 @@ function stepCommand(document: TextDocument, currentPos: Position, forward: bool return nextCmdPos; } -function checkProofForward(context : ExtensionContext) { - - //Checking workspace - const openEditor : TextEditor | undefined = window.activeTextEditor; - if(!openEditor) - return; - - const proofState : Position | undefined = context.workspaceState.get('proofState'); - const panel : WebviewPanel | undefined = context.workspaceState.get('panel'); - if (!proofState || !panel) { - console.log('checkProofForward : Workspace variables are not properly defined'); - return; - } - - let newPos = stepCommand(openEditor.document, proofState, true); - if(newPos) - lpRefresh(context, newPos, panel, openEditor); -} - -function checkProofBackward(context : ExtensionContext) { - - //Checking workspace - const openEditor : TextEditor | undefined = window.activeTextEditor; - if(!openEditor) - return; - - const proofState : Position | undefined = context.workspaceState.get('proofState'); - const panel : WebviewPanel | undefined = context.workspaceState.get('panel'); - if (!proofState || !panel) { - console.log('checkProofBackward : Workspace variables are not properly defined'); +/* +This function is called when the server communicates new Goals to the client +The function checks first that the Goal panel is open and open a new one otherwise +*/ +function refreshGoals(panel: WebviewPanel | null | undefined, editor: TextEditor | undefined, proofState: Position, context: ExtensionContext) { + if (!editor) { return; } - let newPos = stepCommand(openEditor.document, proofState, false); - - //Case the end has not been reached - if(newPos) - lpRefresh(context, newPos, panel, openEditor); -} - -function checkProofUntilCursor(context : ExtensionContext) { - - //Checking workspace - const openEditor : TextEditor | undefined = window.activeTextEditor; - if(!openEditor) - return; - - const proofState : Position | undefined = context.workspaceState.get('proofState'); - const panel : WebviewPanel | undefined = context.workspaceState.get('panel'); - - if (!proofState || !panel) { - console.log('checkProofUntilCursor : workspace variables are not properly defined'); - return; + // Check the panel is open. Recreate it otherwise + if (panel == null || !panel) { + createInfoPanel(context); + panel = context.workspaceState.get('panel')!; } - - //The current position of the cursor - let cursorPosition : Position = openEditor.selection.active; - if (proofState.line == cursorPosition.line) - return; - - //To simplify the code, proof states are always at the beggining of the highlighted line - //So must be the cursor position since it is the new proof state - if (cursorPosition.character != 0) - cursorPosition = new Position(cursorPosition.line, 0); - - context.workspaceState.update('proofState', cursorPosition); //proof state is set to the cursor position - - refreshGoals(panel, openEditor, cursorPosition, context); //Goals panel is refreshed - highlight(context, cursorPosition, openEditor); -} - -function refreshGoals(panel : WebviewPanel, editor : TextEditor | undefined, proofState : Position, context : ExtensionContext) { - - if(!editor) - return; - - const styleUri = panel.webview.asWebviewUri(Uri.joinPath(context.extensionUri, 'media', 'styles.css')) - sendGoalsRequest(proofState, panel, editor.document.uri, styleUri); + const styleUri = panel!.webview.asWebviewUri(Uri.joinPath(context.extensionUri, 'media', 'styles.css')) + sendGoalsRequest(proofState, panel!, editor.document.uri, styleUri); } // returns the HTML code of goals environment -function getGoalsEnvContent(goals : Goal[]){ +function getGoalsEnvContent(goals: Goal[]) { - if(goals.length == 0) + if (goals.length == 0) return "No goals"; return goals.map((curGoal, itr) => { let goalStr = curGoal.typeofgoal == "Typ" ? (curGoal as TypGoal).type : (curGoal as UnifGoal).constr; return '
' + - curGoal.hyps.map((hyp) => { - return `` + - `` + - `${hyp.htype}
`; - }).reduce((acc, cur) => acc + cur, "") + - '
' + - '
' + - `
` + - `` + + curGoal.hyps.map((hyp) => { + return `` + `` + - `${goalStr}` + - `

` + - `
`; + `${hyp.htype}
`; + }).reduce((acc, cur) => acc + cur, "") + + '' + + '
' + + `
` + + `` + + `` + + `${goalStr}` + + `

` + + `
`; }).reduce((acc, cur) => acc + cur, ""); } // number of write operations todo on the pseudoterminal let ptyWriteCnt = 0; -function updateTerminalText(logstr: string){ +function updateTerminalText(logstr: string) { logstr = logstr.replace(/^[\n \t\r]*(\u001b\[[0-9]+m)[\n \t\r]*/g, "$1") - .replace(/[\n \t\r]*(\u001b\[[0-9]+m)[\n \t\r]*$/g, "$1"); + .replace(/[\n \t\r]*(\u001b\[[0-9]+m)[\n \t\r]*$/g, "$1"); const termName = "Lambdapi Debug"; const clearTextSeq = '\x1b[2J\x1b[3J\x1b[;H'; let term = window.terminals.find((t) => t.name == termName); - if(!term){ + if (!term) { const writeEmitter = new EventEmitter(); - const pty : Pseudoterminal = { + const pty: Pseudoterminal = { onDidWrite: writeEmitter.event, - open: () => {}, - close: () => {}, + open: () => { }, + close: () => { }, handleInput: (data: string) => { - if(ptyWriteCnt > 0){ + if (ptyWriteCnt > 0) { ptyWriteCnt--; data = data.replace(/\r/g, '\r\n'); writeEmitter.fire(data); } } }; - term = window.createTerminal({name: termName, pty}); + term = window.createTerminal({ name: termName, pty }); term.show(true); } @@ -530,12 +598,12 @@ function updateTerminalText(logstr: string){ } // Returns the HTML code of the panel and the inset ccontent -function buildGoalsContent(goals : Goal[], styleUri : Uri) { - - let header, footer : String; +function buildGoalsContent(goals: Goal[], styleUri: Uri) { + + let header, footer: String; // get the HTML code of goals environment - let codeEnvGoals : String = getGoalsEnvContent(goals); + let codeEnvGoals: String = getGoalsEnvContent(goals); // Use #FA8072 color too? @@ -556,62 +624,63 @@ function buildGoalsContent(goals : Goal[], styleUri : Uri) { `; } -export interface TextDocumentIdent{ - uri : String +export interface TextDocumentIdent { + uri: String } export interface ParamsGoals { - textDocument : TextDocumentIdent // current text document - position : Position // position to get goals + textDocument: TextDocumentIdent // current text document + position: Position // position to get goals } export interface Env { - hname : String // hypothesis name - htype : String // hypothesis type + hname: String // hypothesis name + htype: String // hypothesis type } export interface Goal { - typeofgoal : String // type of goal, values defined in lsp_base.ml - hyps : Env[] // hypotheses + typeofgoal: String // type of goal, values defined in lsp_base.ml + hyps: Env[] // hypotheses } export interface UnifGoal extends Goal { - constr : String + constr: String } export interface TypGoal extends Goal { - gid : String // goal id - type : String // goals + gid: String // goal id + type: String // goals } export interface GoalResp { - goals : Goal[] - logs : string + goals: Goal[] + logs: string } -function sendGoalsRequest(position: Position, panel : WebviewPanel, docUri : Uri, styleUri : Uri) { +// Build a request, send it to the server and update the Goals panel when the answer is received +function sendGoalsRequest(position: Position, panel: WebviewPanel, docUri: Uri, styleUri: Uri) { - let doc = {uri : docUri.toString()} - let cursor = {textDocument : doc, position : position}; + let doc = { uri: docUri.toString() } + let cursor = { textDocument: doc, position: position }; const req = new RequestType("proof/goals"); client.sendRequest(req, cursor).then((goals) => { - + updateTerminalText(goals.logs); - if(goals.goals) { + if (goals.goals) { let goal_render = buildGoalsContent(goals.goals, styleUri); panel.webview.html = goal_render // Disabled as this is experimental - // let wb = window.createWebviewTextEditorInset(window.activeTextEditor, line, height); - // wb.webview.html = panel.webview.html; + // let wb = window.createWebviewTextEditorInset(window.activeTextEditor, line, height); + // wb.webview.html = panel.webview.html; } else { panel.webview.html = buildGoalsContent([], styleUri); } }, () => { panel.webview.html = buildGoalsContent([], styleUri); }); } - -export function deactivate(): Thenable | undefined { +// Deactivate the Lambdapi extension. Stop the client. +export function deactivateClientLSP(): Thenable | undefined { if (!client) { return undefined; } diff --git a/editors/vscode/src/config.ts b/editors/vscode/src/config.ts new file mode 100644 index 000000000..05c43f95e --- /dev/null +++ b/editors/vscode/src/config.ts @@ -0,0 +1,62 @@ +import { DocumentSelector, ExtensionContext, workspace } from "vscode"; + +export interface LspServerConfig { + client_version: string; + eager_diagnostics: boolean; + goal_after_tactic: boolean; + show_info_messages: boolean; + show_notices_as_diagnostics: boolean; + admit_on_bad_qed: boolean; + debug: boolean; + unicode_completion: "off" | "normal" | "extended"; + max_errors: number; + pp_type: 0 | 1 | 2; + show_stats_on_hover: boolean; + show_loc_info_on_hover: boolean; + check_only_on_request: boolean; +} + +export namespace LspServerConfig { + export function create( + client_version: string, + wsConfig: any + ): LspServerConfig { + return { + client_version: client_version, + eager_diagnostics: wsConfig.eager_diagnostics, + goal_after_tactic: wsConfig.goal_after_tactic, + show_info_messages: wsConfig.show_info_messages, + show_notices_as_diagnostics: wsConfig.show_notices_as_diagnostics, + admit_on_bad_qed: wsConfig.admit_on_bad_qed, + debug: wsConfig.debug, + unicode_completion: wsConfig.unicode_completion, + max_errors: wsConfig.max_errors, + pp_type: wsConfig.pp_type, + show_stats_on_hover: wsConfig.show_stats_on_hover, + show_loc_info_on_hover: wsConfig.show_loc_info_on_hover, + check_only_on_request: wsConfig.check_only_on_request, + }; + } +} + +export enum ShowGoalsOnCursorChange { + Never = 0, + OnMouse = 1, + OnMouseAndKeyboard = 2, + OnMouseKeyboardCommand = 3, +} + +export interface LspClientConfig { + show_goals_on: ShowGoalsOnCursorChange; +} + +export namespace LspClientConfig { + export function create(wsConfig: any): LspClientConfig { + let obj: LspClientConfig = { show_goals_on: wsConfig.show_goals_on }; + return obj; + } +} +export const LSPDocumentSelector: DocumentSelector = [ + { language: "lambdapi" }, + { language: "markdown", pattern: "**/*.lp" }, +]; diff --git a/editors/vscode/src/tsconfig.json b/editors/vscode/src/tsconfig.json new file mode 100644 index 000000000..d71942ba5 --- /dev/null +++ b/editors/vscode/src/tsconfig.json @@ -0,0 +1,13 @@ +{ +// "extends": "../tsconfig-base.json", + "compilerOptions": { + "module": "CommonJS", + "target": "ESNext" + }, + + "files": [ + "client.ts", + "browser.ts" + ], + // "include": ["**/*.ts", "../lib/**/*.ts"] +} diff --git a/editors/vscode/tsconfig-base.json b/editors/vscode/tsconfig-base.json new file mode 100644 index 000000000..6c7734037 --- /dev/null +++ b/editors/vscode/tsconfig-base.json @@ -0,0 +1,11 @@ +{ + "compilerOptions": { + "sourceMap": true, + "strict": true, + "rootDir": ".", + "outDir": "out", + // "composite": true, + // "noEmit": true, + "skipLibCheck": true + } +} diff --git a/editors/vscode/tsconfig.json b/editors/vscode/tsconfig.json index 644ea34c9..254128778 100644 --- a/editors/vscode/tsconfig.json +++ b/editors/vscode/tsconfig.json @@ -5,10 +5,12 @@ "outDir": "out", "sourceMap": true, "strict": true, - "rootDir": "." + "rootDir": ".", + "skipLibCheck": true }, "files": [ - "src/client.ts" + "src/client.ts", + "src/browser.ts" ], // Default if not specified is node_modules, out, etc... "exclude": [