Make refresh interval 5 minutes, restore refresh button.

Author: ian-r-rose

package.json

@@ -46,7 +46,7 @@
     "@jupyterlab/coreutils": "^2.1.0",
     "@jupyterlab/docmanager": "^0.18.0",
     "@jupyterlab/docregistry": "^0.18.0",
-    "@jupyterlab/filebrowser": "^0.18.0",
+    "@jupyterlab/filebrowser": "^0.18.2",
     "@jupyterlab/observables": "^2.0.3",
     "@jupyterlab/services": "^3.1.0",
     "@phosphor/algorithm": "^1.1.2",

src/browser.ts

@@ -111,6 +111,18 @@ export class GitHubFileBrowser extends Widget {
     this._launchBinderButton.addClass('jp-GitHub-toolbar-item');
     this._browser.toolbar.addItem('binder', this._launchBinderButton);
 
+    // Add our own refresh button, since the other one is hidden
+    // via CSS.
+    let refresher = new ToolbarButton({
+      iconClassName: 'jp-RefreshIcon jp-Icon jp-Icon-16',
+      onClick: () => {
+        this._browser.model.refresh();
+      },
+      tooltip: 'Refresh File List'
+    });
+    refresher.addClass('jp-GitHub-toolbar-item');
+    this._browser.toolbar.addItem('gh-refresher', refresher);
+
     // Set up a listener to check if we can launch mybinder.
     this._browser.model.pathChanged.connect(
       this._onPathChanged,

src/index.ts

@@ -60,9 +60,14 @@ function activateFileBrowser(
   const drive = new GitHubDrive(app.docRegistry);
   manager.services.contents.addDrive(drive);
 
+  // Create the embedded filebrowser. GitHub repos likely
+  // don't need as often of a refresh interval as normal ones,
+  // and rate-limiting can be an issue, so we give a 5 minute
+  // refresh interval.
   const browser = factory.createFileBrowser(NAMESPACE, {
     commands,
-    driveName: drive.name
+    driveName: drive.name,
+    refreshInterval: 300000
   });
 
   const gitHubBrowser = new GitHubFileBrowser(browser, drive);