message: Debounce orange bars.
diff: -import { Diagnostic, DiagnosticCollection, DiagnosticSeverity, Disposable, ExtensionContext,
  - languages, OverviewRulerLane, Range, TextEditorDecorationType, Uri, window, workspace } from 'vscode';
  +import { Disposable, ExtensionContext, OverviewRulerLane, Range, TextEditorDecorationType, window, workspace } from 'vscode';
  import { LeanClient } from './leanclient';
  import { ServerProgress } from './leanclientTypes';
  +class LeanFileTaskGutter {
  + private timeout: NodeJS.Timeout
  +
  + constructor(private uri: string, private decoration: TextEditorDecorationType, private processed: number | undefined) {
  + this.schedule(100)
  + }
  +
  + setProcessed(processed: number | undefined) {
  + if (processed === this.processed) return;
  + const oldProcessed = this.processed;
  + this.processed = processed;
  + if (processed === undefined) {
  + if (this.timeout !== undefined) {
  + clearTimeout(this.timeout)
  + this.timeout = undefined;
  + }
  + this.updateDecos();
  + } else if (this.timeout === undefined) {
  + this.schedule(oldProcessed === undefined ? 500 : 20)
  + }
  + }
  +
  + private schedule(ms: number) {
  + this.timeout = setTimeout(() => {
  + this.timeout = undefined
  + this.updateDecos()
  + }, ms)
  + }
  +
  + private updateDecos() {
  + for (const editor of window.visibleTextEditors) {
  + if (editor.document.uri.toString() === this.uri) {
  + editor.setDecorations(this.decoration, this.processed === undefined ? [] : [{
  + range: new Range(this.processed, 0, editor.document.lineCount, 0),
  + hoverMessage: 'busily processing...',
  + }]);
  + }
  + }
  + }
  +}
  +
  export class LeanTaskGutter implements Disposable {
  private decoration: TextEditorDecorationType;
  + private status: ServerProgress;
  + private gutters: { [uri: string]: LeanFileTaskGutter } = {};
  private subscriptions: Disposable[] = [];
  constructor(client: LeanClient, context: ExtensionContext) {
  @@ -20,18 +62,29 @@ export class LeanTaskGutter implements Disposable {
  gutterIconSize: 'contain',
  });
  - this.subscriptions.push(client.progressChanged(
  - (status) => this.updateDecos(status)));
  + this.subscriptions.push(
  + window.onDidChangeVisibleTextEditors(() => this.updateDecos()),
  + client.progressChanged((status) => {
  + this.status = status;
  + this.updateDecos()
  + }));
  }
  - private updateDecos(status: ServerProgress) {
  + private updateDecos() {
  + const uris: { [uri: string]: boolean } = {}
  for (const editor of window.visibleTextEditors) {
  - const line = status[editor.document.uri.toString()];
  - editor.setDecorations(this.decoration, line === undefined ? [] : [{
  - range: new Range(line, 0, editor.document.lineCount, 0),
  - hoverMessage: 'busily processing...',
  - }]);
  + if (editor.document.languageId !== 'lean4' && editor.document.languageId !== 'lean') continue;
  + const uri = editor.document.uri.toString();
  + uris[uri] = true
  + const processed = uri in this.status ? this.status[uri] : 0
  + if (this.gutters[uri]) {
  + this.gutters[uri].setProcessed(processed)
  + } else {
  + this.gutters[uri] = new LeanFileTaskGutter(uri, this.decoration, processed)
  + }
  }
  + Object.getOwnPropertyNames(this.gutters).forEach((uri) =>
  + uris[uri] || (this.gutters[uri] = undefined));
  }
  dispose(): void {
  