|
@@ -2,7 +2,7 @@
|
|
|
// Distributed under the terms of the Modified BSD License.
|
|
|
|
|
|
import {
|
|
|
- IChangedArgs
|
|
|
+ IChangedArgs, PathExt
|
|
|
} from '@jupyterlab/coreutils';
|
|
|
|
|
|
import {
|
|
@@ -56,8 +56,13 @@ class FileEditor extends CodeEditorWrapper implements DocumentRegistry.IReadyWid
|
|
|
if (context.model.modelDB.isCollaborative) {
|
|
|
let modelDB = context.model.modelDB;
|
|
|
modelDB.connected.then(() => {
|
|
|
+ let collaborators = modelDB.collaborators;
|
|
|
+ if (!collaborators) {
|
|
|
+ return;
|
|
|
+ }
|
|
|
+
|
|
|
// Setup the selection style for collaborators
|
|
|
- let localCollaborator = modelDB.collaborators.localCollaborator;
|
|
|
+ let localCollaborator = collaborators.localCollaborator;
|
|
|
this.editor.uuid = localCollaborator.sessionId;
|
|
|
|
|
|
this.editor.selectionStyle = {
|
|
@@ -65,7 +70,7 @@ class FileEditor extends CodeEditorWrapper implements DocumentRegistry.IReadyWid
|
|
|
color: localCollaborator.color
|
|
|
};
|
|
|
|
|
|
- modelDB.collaborators.changed.connect(this._onCollaboratorsChanged, this);
|
|
|
+ collaborators.changed.connect(this._onCollaboratorsChanged, this);
|
|
|
// Trigger an initial onCollaboratorsChanged event.
|
|
|
this._onCollaboratorsChanged();
|
|
|
});
|
|
@@ -153,7 +158,7 @@ class FileEditor extends CodeEditorWrapper implements DocumentRegistry.IReadyWid
|
|
|
const path = this._context.path;
|
|
|
|
|
|
editor.model.mimeType = this._mimeTypeService.getMimeTypeByFilePath(path);
|
|
|
- this.title.label = path.split(':').pop().split('/').pop();
|
|
|
+ this.title.label = PathExt.basename(path.split(':').pop()!);
|
|
|
}
|
|
|
|
|
|
/**
|
|
@@ -163,8 +168,12 @@ class FileEditor extends CodeEditorWrapper implements DocumentRegistry.IReadyWid
|
|
|
private _onCollaboratorsChanged(): void {
|
|
|
// If there are selections corresponding to non-collaborators,
|
|
|
// they are stale and should be removed.
|
|
|
+ let collaborators = this._context.model.modelDB.collaborators;
|
|
|
+ if (!collaborators) {
|
|
|
+ return;
|
|
|
+ }
|
|
|
for (let key of this.editor.model.selections.keys()) {
|
|
|
- if (!this._context.model.modelDB.collaborators.has(key)) {
|
|
|
+ if (!collaborators.has(key)) {
|
|
|
this.editor.model.selections.delete(key);
|
|
|
}
|
|
|
}
|