diff --git a/package.json b/package.json index 03f4087..88f8694 100644 --- a/package.json +++ b/package.json @@ -473,7 +473,25 @@ "highContrast": "#d8d8d850" } } - ] + ], + "viewsContainers": { + "activitybar": [ + { + "id": "tlaplus", + "title": "TLA+", + "icon": "resources/images/tlaplus.svg" + } + ] + }, + "views": { + "tlaplus": [ + { + "id": "tlaplus.tlaps-current-proof-obligation", + "name": "Current Proof Obligation", + "type": "webview" + } + ] + } }, "scripts": { "vscode:prepublish": "npm run compile -- --production", diff --git a/resources/images/tlaplus.svg b/resources/images/tlaplus.svg new file mode 100644 index 0000000..1ee7f25 --- /dev/null +++ b/resources/images/tlaplus.svg @@ -0,0 +1,66 @@ + + + + diff --git a/src/main.ts b/src/main.ts index 0ec16aa..c50a429 100644 --- a/src/main.ts +++ b/src/main.ts @@ -6,8 +6,11 @@ import { showTlcOutput, checkModelCustom, CMD_CHECK_MODEL_RUN_AGAIN, runLastCheckAgain } from './commands/checkModel'; import { CMD_RUN_REPL, launchRepl, REPLTerminalProfileProvider } from './commands/runRepl'; -import { TLAPLUS_DEBUG_LAUNCH_CHECKNDEBUG, TLAPLUS_DEBUG_LAUNCH_CUSTOMCHECKNDEBUG, TLAPLUS_DEBUG_LAUNCH_DEBUG,TLAPLUS_DEBUG_LAUNCH_SMOKE, - TLADebugAdapterServerDescriptorFactory, checkAndDebugSpec, checkAndDebugSpecCustom, attachDebugger, smokeTestSpec +import { + TLAPLUS_DEBUG_LAUNCH_CHECKNDEBUG, TLAPLUS_DEBUG_LAUNCH_CUSTOMCHECKNDEBUG, + TLAPLUS_DEBUG_LAUNCH_DEBUG,TLAPLUS_DEBUG_LAUNCH_SMOKE, + TLADebugAdapterServerDescriptorFactory, checkAndDebugSpec, checkAndDebugSpecCustom, + attachDebugger, smokeTestSpec } from './debugger/debugging'; import { CMD_EVALUATE_SELECTION, evaluateSelection, CMD_EVALUATE_EXPRESSION, evaluateExpression } from './commands/evaluateExpression'; @@ -26,6 +29,7 @@ import { TlaDeclarationsProvider, TlaDefinitionsProvider } from './declarations/ import { TlaDocumentInfos } from './model/documentInfo'; import { syncTlcStatisticsSetting, listenTlcStatConfigurationChanges } from './commands/tlcStatisticsCfg'; import { TlapsClient } from './tlaps'; +import { TlapsProofObligationView } from './webview/tlapsCurrentProofObligationView'; const TLAPLUS_FILE_SELECTOR: vscode.DocumentSelector = { scheme: 'file', language: LANG_TLAPLUS }; const TLAPLUS_CFG_FILE_SELECTOR: vscode.DocumentSelector = { scheme: 'file', language: LANG_TLAPLUS_CFG }; @@ -42,6 +46,7 @@ let tlapsClient: TlapsClient | undefined; * Extension entry point. */ export function activate(context: vscode.ExtensionContext): void { + const tlapsProofObligationView = new TlapsProofObligationView(); diagnostic = vscode.languages.createDiagnosticCollection(LANG_TLAPLUS); context.subscriptions.push( vscode.commands.registerCommand( @@ -124,7 +129,7 @@ export function activate(context: vscode.ExtensionContext): void { (uri) => checkAndDebugSpec(uri, diagnostic, context) ), vscode.commands.registerCommand( - TLAPLUS_DEBUG_LAUNCH_CUSTOMCHECKNDEBUG, + TLAPLUS_DEBUG_LAUNCH_CUSTOMCHECKNDEBUG, (uri) => checkAndDebugSpecCustom(uri, diagnostic, context) ), vscode.commands.registerCommand( @@ -159,9 +164,14 @@ export function activate(context: vscode.ExtensionContext): void { // 1 1 1 2 (wordRange.end.character /** + 1 */))) : undefined; } - }) + } + ), + vscode.window.registerWebviewViewProvider( + TlapsProofObligationView.viewType, + tlapsProofObligationView, + ) ); - tlapsClient = new TlapsClient(context); + tlapsClient = new TlapsClient(context, tlapsProofObligationView); syncTlcStatisticsSetting() .catch((err) => console.error(err)) .then(() => listenTlcStatConfigurationChanges(context.subscriptions)); diff --git a/src/model/tlaps.ts b/src/model/tlaps.ts new file mode 100644 index 0000000..bf29f20 --- /dev/null +++ b/src/model/tlaps.ts @@ -0,0 +1,15 @@ +import { Location } from 'vscode-languageclient/node'; + +export interface TlapsProofObligationResult { + prover: string; + meth: string; + status: string; + duration: number; + obligation: string | null; // Non-null, if prover failed. +} + +export interface TlapsProofObligationState { + location: Location; + obligation: string; + results: TlapsProofObligationResult[]; +} diff --git a/src/tlaps.ts b/src/tlaps.ts index f94ee32..360208b 100644 --- a/src/tlaps.ts +++ b/src/tlaps.ts @@ -1,3 +1,12 @@ +// TODO: Click on the proof gutter icons. +// - https://github.com/microsoft/vscode/issues/5455 +// - https://github.com/microsoft/vscode/issues/175945#issuecomment-1466438453 +// +// TODO: Tree View to show the proof. +// https://code.visualstudio.com/api/extension-guides/tree-view +// https://github.com/microsoft/vscode/issues/103403 +// Also show WebviewView to show a custom content in a sidebar. +// import * as vscode from 'vscode'; import { DocumentUri, @@ -7,6 +16,8 @@ import { TransportKind, VersionedTextDocumentIdentifier } from 'vscode-languageclient/node'; +import { TlapsProofObligationView } from './webview/tlapsCurrentProofObligationView'; +import { TlapsProofObligationState } from './model/tlaps'; interface ProofStateMarker { range: vscode.Range; @@ -29,7 +40,10 @@ export class TlapsClient { ]; private proofStateDecorationTypes = new Map(); - constructor(private context: vscode.ExtensionContext) { + constructor( + private context: vscode.ExtensionContext, + private tlapsProofObligationView: TlapsProofObligationView, + ) { context.subscriptions.push(vscode.commands.registerTextEditorCommand( 'tlaplus.tlaps.check-step', (te, ed, args) => { @@ -130,6 +144,12 @@ export class TlapsClient { 'tlaplus/tlaps/proofStates', this.proofStateNotifHandler.bind(this) )); + this.context.subscriptions.push(this.client.onNotification( + 'tlaplus/tlaps/currentProofObligation', + (oblState: TlapsProofObligationState) => { + this.tlapsProofObligationView.showProofObligation(oblState); + } + )); this.client.start(); } diff --git a/src/webview/tlapsCurrentProofObligationView.ts b/src/webview/tlapsCurrentProofObligationView.ts new file mode 100644 index 0000000..c2c5a74 --- /dev/null +++ b/src/webview/tlapsCurrentProofObligationView.ts @@ -0,0 +1,66 @@ +import * as vscode from 'vscode'; +import { TlapsProofObligationState } from '../model/tlaps'; +import { URI } from 'vscode-uri'; + +export class TlapsProofObligationView implements vscode.WebviewViewProvider { + public static readonly viewType = 'tlaplus.tlaps-current-proof-obligation'; + private view?: vscode.WebviewView; + private oblState: TlapsProofObligationState | null = null; + + public resolveWebviewView( + webviewView: vscode.WebviewView, + _context: vscode.WebviewViewResolveContext, + _token: vscode.CancellationToken, + ) { + this.view = webviewView; + this.show(); + } + + public showProofObligation(oblState: TlapsProofObligationState | null) { + this.oblState = oblState; + this.show(); + } + + private show() { + if (this.view) { + this.view.webview.html = this.makeHtml(); + } + } + + private makeHtml() { + const header = + ` + + + + + Cat Coding + + `; + const footer = + ` + `; + let content = '

No obligation selected.

'; + if (this.oblState) { + const loc = this.oblState.location; + const uri = URI.parse(loc.uri); + content = `

${uri.path.split(/\/|\\/).pop()}

`; + if (loc.range.start.line === loc.range.end.line) { + content += `

Line: ${loc.range.start.line}

`; + } else { + content += `

Lines: ${loc.range.start.line}-${loc.range.end.line}

`; + } + if (this.oblState.results) { + content += ''; + } else { + content += '

Not checked yet.

'; + } + content += `
${this.oblState.obligation}
`; + } + return header + content + footer; + } +}