fix #2315: fine grain marker tree computation

Signed-off-by: Anton Kosyakov <anton.kosyakov@typefox.io>
eclipse-theia · Jul 9, 2018 · 32339fe · 32339fe
1 parent b990b2f
commit 32339fe
Show file tree

Hide file tree

Showing 4 changed files with 82 additions and 69 deletions.
diff --git a/packages/core/src/browser/tree/tree-widget.tsx b/packages/core/src/browser/tree/tree-widget.tsx
@@ -128,7 +128,6 @@ export class TreeWidget extends ReactWidget implements StatefulWidget {
         ]);
         setTimeout(() => {
             this.updateRows();
-            this.updateScrollToRow();
             this.updateDecorations();
         });
     }
@@ -157,7 +156,7 @@ export class TreeWidget extends ReactWidget implements StatefulWidget {
         } else {
             this.rows = new Map();
         }
-        this.update();
+        this.updateScrollToRow();
     }
 
     protected scrollToRow: number | undefined;

diff --git a/packages/core/src/browser/tree/tree.ts b/packages/core/src/browser/tree/tree.ts
@@ -246,13 +246,34 @@ export class TreeImpl implements Tree {
         if (CompositeTreeNode.is(node)) {
             const { children } = node;
             children.forEach((child, index) => {
-                const parent = node;
-                const previousSibling = children[index - 1];
-                const nextSibling = children[index + 1];
-                Object.assign(child, { parent, previousSibling, nextSibling });
+                this.setParent(child, index, node);
                 this.addNode(child);
             });
         }
     }
 
+    protected setParent(child: TreeNode, index: number, parent: CompositeTreeNode): void {
+        const previousSibling = parent.children[index - 1];
+        const nextSibling = parent.children[index + 1];
+        Object.assign(child, { parent, previousSibling, nextSibling });
+    }
+
+    protected addChild(parent: CompositeTreeNode, child: TreeNode): void {
+        const index = parent.children.findIndex(value => value.id === child.id);
+        if (index !== -1) {
+            (parent.children as TreeNode[]).splice(index, 1, child);
+            this.setParent(child, index, parent);
+        } else {
+            (parent.children as TreeNode[]).push(child);
+            this.setParent(child, parent.children.length - 1, parent);
+        }
+    }
+
+    protected removeChild(parent: CompositeTreeNode, child: TreeNode): void {
+        const index = parent.children.findIndex(value => value.id === child.id);
+        if (index !== -1) {
+            (parent.children as TreeNode[]).splice(index, 1);
+        }
+    }
+
 }
diff --git a/packages/markers/src/browser/marker-manager.ts b/packages/markers/src/browser/marker-manager.ts
@@ -21,6 +21,8 @@ import { StorageService } from '@theia/core/lib/browser/storage-service';
 import { FileSystemWatcher, FileChangeType } from '@theia/filesystem/lib/browser/filesystem-watcher';
 import { Marker } from '../common/marker';
 
+const debounce = require("lodash.debounce");
+
 /*
  * argument to the `findMarkers` method.
  */
@@ -150,7 +152,8 @@ export abstract class MarkerManager<D extends object> {
         }
     }
 
-    protected saveMarkersToStorage() {
+    protected readonly saveMarkersToStorage = debounce(() => this.doSaveMarkersToStorage(), 500);
+    protected doSaveMarkersToStorage(): void {
         const key = this.getStorageKey();
         if (key) {
             const result: Uri2MarkerEntry[] = [];

diff --git a/packages/markers/src/browser/marker-tree.ts b/packages/markers/src/browser/marker-tree.ts
@@ -37,7 +37,7 @@ export abstract class MarkerTree<T extends object> extends TreeImpl {
     ) {
         super();
 
-        this.toDispose.push(markerManager.onDidChangeMarkers(() => this.refresh()));
+        this.toDispose.push(markerManager.onDidChangeMarkers(uri => this.refreshMarkerInfo(uri)));
 
         this.root = <MarkerRootNode>{
             visible: false,
@@ -49,73 +49,63 @@ export abstract class MarkerTree<T extends object> extends TreeImpl {
         };
     }
 
-    resolveChildren(parent: CompositeTreeNode): Promise<TreeNode[]> {
-        if (MarkerRootNode.is(parent)) {
-            return this.getMarkerInfoNodes((parent as MarkerRootNode));
-        } else if (MarkerInfoNode.is(parent)) {
-            return this.getMarkerNodes(parent);
+    protected async refreshMarkerInfo(uri: URI): Promise<void> {
+        const id = uri.toString();
+        const existing = this.getNode(id);
+        const markers = this.markerManager.findMarkers({ uri });
+        if (markers.length <= 0) {
+            if (MarkerInfoNode.is(existing)) {
+                this.removeChild(existing.parent, existing);
+                this.removeNode(existing);
+                this.fireChanged();
+            }
+            return;
         }
-        return super.resolveChildren(parent);
+        const node = MarkerInfoNode.is(existing) ? existing : await this.createMarkerInfo(id, uri);
+        this.addChild(node.parent, node);
+        const children = this.getMarkerNodes(node, markers);
+        node.numberOfMarkers = markers.length;
+        this.setChildren(node, children);
     }
 
-    async getMarkerInfoNodes(parent: MarkerRootNode): Promise<MarkerInfoNode[]> {
-        const uriNodes: MarkerInfoNode[] = [];
-        if (this.root && MarkerRootNode.is(this.root)) {
-            for (const uriString of this.markerManager.getUris()) {
-                const id = 'markerInfo-' + uriString;
-                const uri = new URI(uriString);
-                const label = await this.labelProvider.getName(uri);
-                const icon = await this.labelProvider.getIcon(uri);
-                const description = await this.labelProvider.getLongName(uri.parent);
-                const numberOfMarkers = this.markerManager.findMarkers({ uri }).length;
-                if (numberOfMarkers > 0) {
-                    const cachedMarkerInfo = this.getNode(id);
-                    if (cachedMarkerInfo && MarkerInfoNode.is(cachedMarkerInfo)) {
-                        cachedMarkerInfo.numberOfMarkers = numberOfMarkers;
-                        uriNodes.push(cachedMarkerInfo);
-                    } else {
-                        uriNodes.push({
-                            children: [],
-                            expanded: true,
-                            uri,
-                            id,
-                            name: label,
-                            icon,
-                            description,
-                            parent,
-                            selected: false,
-                            numberOfMarkers
-                        });
-                    }
-                }
-            }
-        }
-        return Promise.resolve(uriNodes);
+    protected async createMarkerInfo(id: string, uri: URI): Promise<MarkerInfoNode> {
+        const label = await this.labelProvider.getName(uri);
+        const icon = await this.labelProvider.getIcon(uri);
+        const description = await this.labelProvider.getLongName(uri.parent);
+        return {
+            children: [],
+            expanded: true,
+            uri,
+            id,
+            name: label,
+            icon,
+            description,
+            parent: this.root as MarkerRootNode,
+            selected: false,
+            numberOfMarkers: 0
+        };
     }
 
-    getMarkerNodes(parent: MarkerInfoNode): Promise<MarkerNode[]> {
-        const markerNodes: MarkerNode[] = [];
-        const markers = this.markerManager.findMarkers({ uri: parent.uri });
-        for (let i = 0; i < markers.length; i++) {
-            const marker = markers[i];
-            const uri = new URI(marker.uri);
-            const id = uri.toString() + "_" + i;
-            const cachedMarkerNode = this.getNode(id);
-            if (MarkerNode.is(cachedMarkerNode)) {
-                cachedMarkerNode.marker = marker;
-                markerNodes.push(cachedMarkerNode);
-            } else {
-                markerNodes.push({
-                    id,
-                    name: 'marker',
-                    parent,
-                    selected: false,
-                    uri,
-                    marker
-                });
-            }
+    protected getMarkerNodes(parent: MarkerInfoNode, markers: Marker<T>[]): MarkerNode[] {
+        return markers.map((marker, index) =>
+            this.createMarkerNode(marker, index, parent)
+        );
+    }
+    protected createMarkerNode(marker: Marker<T>, index: number, parent: MarkerInfoNode): MarkerNode {
+        const id = parent.id + "_" + index;
+        const existing = this.getNode(id);
+        if (MarkerNode.is(existing)) {
+            existing.marker = marker;
+            return existing;
         }
-        return Promise.resolve(markerNodes);
+        return {
+            id,
+            name: 'marker',
+            parent,
+            selected: false,
+            uri: parent.uri,
+            marker
+        };
     }
 }