Skip to content

Commit

Permalink
fix: #115 : Infoview not working for external file
Browse files Browse the repository at this point in the history
  • Loading branch information
@lovettchris
lovettchris committed Feb 8, 2022
1 parent a63c601 commit fa2b871
Show file tree
Hide file tree
Showing 5 changed files with 91 additions and 52 deletions.
39 changes: 14 additions & 25 deletions vscode-lean4/src/infoview.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,22 +52,14 @@ export class InfoProvider implements Disposable {

private stylesheet: string = '';
private autoOpened: boolean = false;
private clients: LeanClient[] = [];
private clientProvider: LeanClientProvider;

// Subscriptions are counted and only disposed of when count becomes 0.
private serverNotifSubscriptions: Map<string, [number, Disposable[]]> = new Map();
private clientNotifSubscriptions: Map<string, [number, Disposable[]]> = new Map();

private rpcSessions: Map<string, RpcSession> = new Map();

private findClient(uri:string) : LeanClient{
for (const client of this.clients) {
if (uri.startsWith(client.getWorkspaceFolder()))
return client
}
return null
}

private subscribeDidChangeNotification(client: LeanClient, method: string){
const h = client.didChange((params) => {
void this.webviewPanel?.api.sentClientNotification(method, params);
Expand Down Expand Up @@ -99,14 +91,14 @@ export class InfoProvider implements Disposable {

private editorApi : EditorApi = {
sendClientRequest: async (uri: string, method: string, params: any): Promise<any> => {
const client = this.findClient(uri);
const client = this.clientProvider.findClient(uri);
if (client) {
return client.sendRequest(method, params);
}
return undefined;
},
sendClientNotification: async (uri: string, method: string, params: any): Promise<void> => {
const client = this.findClient(uri);
const client = this.clientProvider.findClient(uri);
if (client) {
client.sendNotification(method, params);
}
Expand All @@ -124,13 +116,13 @@ export class InfoProvider implements Disposable {
// So we have to add a bunch of event emitters to `LeanClient.`
if (method === 'textDocument/publishDiagnostics') {
const subscriptions : Disposable[] = [];
for (const client of this.clients) {
for (const client of this.clientProvider.getClients()) {
subscriptions.push(this.subscribeDiagnosticsNotification(client, method));
}
this.serverNotifSubscriptions.set(method, [1, subscriptions]);
} else if (method.startsWith('$')) {
const subscriptions : Disposable[] = [];
for (const client of this.clients) {
for (const client of this.clientProvider.getClients()) {
subscriptions.push(this.subscribeCustomNotification(client, method));
}
this.serverNotifSubscriptions.set(method, [1, subscriptions]);
Expand Down Expand Up @@ -162,13 +154,13 @@ export class InfoProvider implements Disposable {

if (method === 'textDocument/didChange') {
const subscriptions : Disposable[] = [];
for (const client of this.clients) {
for (const client of this.clientProvider.getClients()) {
subscriptions.push(this.subscribeDidChangeNotification(client, method));
}
this.clientNotifSubscriptions.set(method, [1, subscriptions]);
} else if (method === 'textDocument/didClose') {
const subscriptions : Disposable[] = [];
for (const client of this.clients) {
for (const client of this.clientProvider.getClients()) {
subscriptions.push(this.subscribeDidCloseNotification(client, method))
}
this.clientNotifSubscriptions.set(method, [1,subscriptions]);
Expand All @@ -195,7 +187,7 @@ export class InfoProvider implements Disposable {
await window.showInformationMessage(`Copied to clipboard: ${text}`);
},
insertText: async (text, kind, tdpp) => {
const client = this.findClient(tdpp.textDocument.uri);
const client = this.clientProvider.findClient(tdpp.textDocument.uri);
if (!client?.running) return;
let uri: Uri | undefined
let pos: Position | undefined
Expand All @@ -206,7 +198,7 @@ export class InfoProvider implements Disposable {
await this.handleInsertText(text, kind, uri, pos);
},
showDocument: async (show) => {
const client = this.findClient(show.uri);
const client = this.clientProvider.findClient(show.uri);
if (!client?.running) return;
void this.revealEditorSelection(
Uri.parse(show.uri),
Expand All @@ -215,7 +207,7 @@ export class InfoProvider implements Disposable {
},

createRpcSession: async uri => {
const client = this.findClient(uri);
const client = this.clientProvider.findClient(uri);
if (!client) return '';
const sessionId = await rpcConnect(client, uri);
const session = new RpcSession(client, sessionId, uri);
Expand All @@ -237,6 +229,7 @@ export class InfoProvider implements Disposable {
};

constructor(private provider: LeanClientProvider, private readonly leanDocs: DocumentSelector, private context: ExtensionContext) {
this.clientProvider = provider;
this.updateStylesheet();

provider.clientAdded((client) => {
Expand Down Expand Up @@ -274,7 +267,6 @@ export class InfoProvider implements Disposable {

private async onClientAdded(client: LeanClient) {

this.clients.push(client);
console.log(`Adding client for workspace: ${client.getWorkspaceFolder()}`);

this.clientSubscriptions.push(
Expand Down Expand Up @@ -425,12 +417,9 @@ export class InfoProvider implements Disposable {
// The infoview gets information about file progress, diagnostics, etc.
// by listening to notifications. Send these notifications when the infoview starts
// so that it has up-to-date information.
// Hmmm: TODO: does this make any sense now with multiple clients?
for(const client of this.clients) {
if (client?.initializeResult) {
await this.webviewPanel.api.serverRestarted(client?.initializeResult);
break;
}
var client = this.clientProvider.findClient(editor.document?.uri?.toString());
if (client?.initializeResult) {
await this.webviewPanel.api.serverRestarted(client?.initializeResult);
}

// await this.sendPosition();
Expand Down
37 changes: 19 additions & 18 deletions vscode-lean4/src/leanclient.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ export class LeanClient implements Disposable {
private outputChannel: OutputChannel;
private storageManager : LocalStorageService;
private workspaceFolder: WorkspaceFolder;

private folderUri: Uri;
private subscriptions: Disposable[] = []

private didChangeEmitter = new EventEmitter<DidChangeTextDocumentParams>()
Expand Down Expand Up @@ -78,11 +78,11 @@ export class LeanClient implements Disposable {
/** Files which are open. */
private isOpen: Set<string> = new Set()

constructor(workspaceFolder: WorkspaceFolder, storageManager : LocalStorageService, outputChannel : OutputChannel) {
constructor(workspaceFolder: WorkspaceFolder, folderUri: Uri, storageManager : LocalStorageService, outputChannel : OutputChannel) {
this.storageManager = storageManager;
this.outputChannel = outputChannel;
this.workspaceFolder = workspaceFolder;

this.workspaceFolder = workspaceFolder; // can be null when opening adhoc files.
this.folderUri = folderUri;
this.subscriptions.push(workspace.onDidChangeConfiguration((e) => this.configChanged(e)));
}

Expand Down Expand Up @@ -111,8 +111,8 @@ export class LeanClient implements Disposable {
// user is requesting an explicit version for this workspace.
options = ['+' + version, '--server']
}
if (this.workspaceFolder) {
options.push('' + this.workspaceFolder.uri.fsPath)
if (this.folderUri) {
options.push('' + this.folderUri.fsPath)
} else {
options.push('untitled')
}
Expand All @@ -130,20 +130,19 @@ export class LeanClient implements Disposable {
language: 'lean4'
}

if (this.workspaceFolder){
documentSelector.scheme = 'file'
documentSelector.pattern = `${this.workspaceFolder.uri.fsPath}/**/*`
} else {
documentSelector.scheme = 'untitled'
if (this.folderUri){
documentSelector.scheme = this.folderUri.scheme
if (this.folderUri.scheme !== 'untitled') {
documentSelector.pattern = `${this.folderUri.fsPath}/**/*`
}
}

const clientOptions: LanguageClientOptions = {
outputChannel: this.outputChannel,
documentSelector: [documentSelector],
workspaceFolder: this.workspaceFolder,
initializationOptions: {
editDelay: getElaborationDelay(),
hasWidgets: true,
editDelay: getElaborationDelay(), hasWidgets: true,
},
middleware: {
handleDiagnostics: (uri, diagnostics, next) => {
Expand Down Expand Up @@ -223,6 +222,7 @@ export class LeanClient implements Disposable {
console.log('client starting');
} else if (s.newState === State.Running) {
console.log('client running');
this.running = true; // may have been auto restarted after it failed.
} else if (s.newState === State.Stopped) {
console.log('client has stopped or it failed to start');
this.running = false;
Expand Down Expand Up @@ -291,15 +291,16 @@ export class LeanClient implements Disposable {
}

async openLean4Document(doc: TextDocument) {
if (this.isOpen.has(doc.uri.toString())) return;
this.isOpen.add(doc.uri.toString())

if (!this.running) return; // there was a problem starting lean server.

if (!this.isSameWorkspace(doc.uri)){
// skip it, this file belongs to a different workspace...
return;
}

if (this.isOpen.has(doc.uri.toString())) return;
this.isOpen.add(doc.uri.toString())
void this.client.sendNotification(DidOpenTextDocumentNotification.type, {
textDocument: {
uri: doc.uri.toString(),
Expand All @@ -311,8 +312,8 @@ export class LeanClient implements Disposable {
}

isSameWorkspace(uri: Uri){
if (this.workspaceFolder) {
if (uri.toString().startsWith(this.workspaceFolder.uri.toString())) {
if (this.folderUri) {
if (uri.toString().startsWith(this.folderUri.toString())) {
// skip it, this file belongs to a different workspace...
return true;
}
Expand All @@ -324,7 +325,7 @@ export class LeanClient implements Disposable {
}

getWorkspaceFolder() : string {
return this.workspaceFolder?.uri.toString();
return this.folderUri?.toString();
}

start(): Promise<void> {
Expand Down
1 change: 1 addition & 0 deletions vscode-lean4/src/taskgutter.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ class LeanFileTaskGutter {

constructor(private uri: string, private decorations: Map<LeanFileProgressKind, [TextEditorDecorationType, string]>, private processed: LeanFileProgressProcessingInfo[]) {
this.schedule(100)
this.processed = []
}

setProcessed(processed: LeanFileProgressProcessingInfo[]) {
Expand Down
64 changes: 56 additions & 8 deletions vscode-lean4/src/utils/clientProvider.ts
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,10 @@
import { Disposable, OutputChannel, workspace, TextDocument, commands, window, EventEmitter, Uri, languages } from 'vscode';
import { Disposable, OutputChannel, workspace, TextDocument, commands, window, EventEmitter, Uri, languages, TextEditor } from 'vscode';
import { LocalStorageService} from './localStorage'
import { LeanInstaller, LeanVersion } from './leanInstaller'
import { LeanClient } from '../leanclient'
import { LeanFileProgressProcessingInfo, RpcConnectParams, RpcKeepAliveParams } from '@lean4/infoview-api';
import * as path from 'path';
import { urlToHttpOptions } from 'url';

// This class ensures we have one LeanClient per workspace folder.
export class LeanClientProvider implements Disposable {
Expand Down Expand Up @@ -41,6 +43,8 @@ export class LeanClientProvider implements Disposable {
commands.registerCommand('lean4.restartServer', () => this.restartActiveClient())
);

workspace.onDidOpenTextDocument((document) => this.didOpenEditor(document));

workspace.onDidChangeWorkspaceFolders((event) => {
for (const folder of event.removed) {
const path = folder.uri.toString();
Expand Down Expand Up @@ -94,6 +98,15 @@ export class LeanClientProvider implements Disposable {
return null;
}

private getVisibleEditor(uri: Uri) : TextEditor | null {
var path = uri.toString();
for (const editor of window.visibleTextEditors) {
if (editor.document.uri.toString() === path){
return editor;
}
}
}

private refreshFileDependencies() {
this.activeClient.refreshFileDependencies(window.activeTextEditor.document);
}
Expand All @@ -103,6 +116,14 @@ export class LeanClientProvider implements Disposable {
}

async didOpenEditor(document: TextDocument) {
if (!this.getVisibleEditor(document.uri)) {
// Sometimes VS code opens a document that has no editor yet.
// For example, this happens when the vs code opens files to get git information
// like this:
// git:/d%3A/Temp/lean_examples/Foo/Foo/Hello.lean.git?%7B%22path%22%3A%22d%3A%5C%5CTemp%5C%5Clean_examples%5C%5CFoo%5C%5CFoo%5C%5CHello.lean%22%2C%22ref%22%3A%22%22%7D
return;
}

// All open .lean files are assumed to be Lean 4 files.
// We need to do this because by default, .lean is associated with language id `lean`,
// i.e. Lean 3. vscode-lean is expected to yield when isLean4Project is true.
Expand All @@ -114,18 +135,36 @@ export class LeanClientProvider implements Disposable {
return;
}

const client = await this.ensureClient(document.uri, null);
let client = await this.ensureClient(document.uri, null);
await client.openLean4Document(document)
}

getClient(uri: Uri){
return this.clients.get(uri.toString());
// Find the client for a given document.
findClient(path: string){
if (path) {
for (const client of this.getClients()) {
if (path.startsWith(client.getWorkspaceFolder()))
return client
}
}
return null
}

getClients() : LeanClient[]{
return Array.from(this.clients.values());
}

getFolderFromUri(uri: Uri) : Uri {
if (uri){
if (uri.scheme === 'untitled'){
// this lean client can handle all untitled documents.
return Uri.from({scheme: 'untitled'});
}
return uri.with({ path: path.posix.dirname(uri.path) });
}
return null;
}

async ensureClient(uri: Uri, versionInfo: LeanVersion | null): Promise<LeanClient> {
let folder = workspace.getWorkspaceFolder(uri);
if (!folder && workspace.workspaceFolders) {
Expand All @@ -137,7 +176,7 @@ export class LeanClientProvider implements Disposable {
});
}

const folderUri = folder ? folder.uri : uri;
const folderUri = folder ? folder.uri : this.getFolderFromUri(uri);
const path = folderUri?.toString();
let client: LeanClient = null;
if (this.clients.has(path)) {
Expand All @@ -146,6 +185,17 @@ export class LeanClientProvider implements Disposable {
} else if (!this.versions.has(path) && !this.pending.has(path)) {
this.pending.set(path, true);
console.log('Creating LeanClient for ' + path);

// We must create a Client before doing the long running testLeanVersion
// so that ensureClient callers have an "optimistic" client to work with.
// This is needed in our constructor where it is calling ensureClient for
// every open file. A workspace could have multiple files open and we want
// to remember all those open files are associated with this client before
// testLeanVersion has completed.
client = new LeanClient(folder, folderUri, this.localStorage, this.outputChannel);
this.subscriptions.push(client);
this.clients.set(path, client);

if (!versionInfo) {
// TODO: what is the uri for untitled documents? Hopefully they get their own special
// LeanClient with some default version...
Expand All @@ -156,12 +206,10 @@ export class LeanClientProvider implements Disposable {
// ignore workspaces that belong to a different version of Lean.
console.log(`Lean4 extension ignoring workspace '${folderUri}' because it is not a Lean 4 workspace.`);
this.pending.delete(path);
this.clients.delete(path);
return;
}

client = new LeanClient(folder, this.localStorage, this.outputChannel);
this.subscriptions.push(client);
this.clients.set(path, client);
client.serverFailed((err) => window.showErrorMessage(err));

// aggregate progress changed events.
Expand Down
2 changes: 1 addition & 1 deletion vscode-lean4/src/utils/leanpkg.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ export class LeanpkgService implements Disposable {
rootPath = folder.uri;
}
if (!rootPath) {
rootPath = window.activeTextEditor.document.uri;
rootPath = window.activeTextEditor?.document.uri;
if (rootPath) {
// remove leaf filename part.
rootPath = Uri.joinPath(rootPath, '..');
Expand Down

0 comments on commit fa2b871

Please sign in to comment.