message: feat: paint each taskgutter range separately
diff: import { Disposable, ExtensionContext, OverviewRulerLane, Range, TextEditorDecorationType, window } from 'vscode';
  import { LeanClient } from './leanclient';
  -import { LeanFileProgressKind } from '@lean4/infoview';
  +import { LeanFileProgressKind, LeanFileProgressProcessingInfo } from '@lean4/infoview';
  class LeanFileTaskGutter {
  private timeout?: NodeJS.Timeout
  - constructor(private uri: string, private decorations: Map<LeanFileProgressKind, [TextEditorDecorationType, string]>, private processed: Map<LeanFileProgressKind, number> | undefined) {
  + constructor(private uri: string, private decorations: Map<LeanFileProgressKind, [TextEditorDecorationType, string]>, private processed: LeanFileProgressProcessingInfo[]) {
  this.schedule(100)
  }
  - setProcessed(processed: Map<LeanFileProgressKind, number> | undefined) {
  + setProcessed(processed: LeanFileProgressProcessingInfo[]) {
  if (processed === this.processed) return;
  const oldProcessed = this.processed;
  this.processed = processed;
  @@ -38,23 +38,16 @@ class LeanFileTaskGutter {
  private updateDecos() {
  for (const editor of window.visibleTextEditors) {
  if (editor.document.uri.toString() === this.uri) {
  - if (this.processed === undefined) {
  - for (const [decoration, _message] of this.decorations.values()) {
  - editor.setDecorations(decoration, [])
  - }
  - } else {
  for (const [kind, [decoration, message]] of this.decorations) {
  - if (this.processed.has(kind)) {
  - const line = this.processed.get(kind)
  -
  - editor.setDecorations(decoration, [{
  - range: new Range(line, 0, editor.document.lineCount, 0),
  + editor.setDecorations(
  + decoration,
  + this.processed
  + .filter(info => (info.kind === undefined ? LeanFileProgressKind.Processing : info.kind) === kind)
  + .map(info => ({
  + range: new Range(info.range.start.line, 0, info.range.end.line, 0),
  hoverMessage: message
  - }])
  - } else {
  - editor.setDecorations(decoration, [])
  - }
  - }
  + }))
  + )
  }
  }
  }
  @@ -67,7 +60,7 @@ class LeanFileTaskGutter {
  export class LeanTaskGutter implements Disposable {
  private decorations: Map<LeanFileProgressKind, [TextEditorDecorationType, string]> = new Map<LeanFileProgressKind, [TextEditorDecorationType, string]>();
  - private status: { [uri: string]: Map<LeanFileProgressKind, number> | undefined } = {};
  + private status: { [uri: string]: LeanFileProgressProcessingInfo[] } = {};
  private gutters: { [uri: string]: LeanFileTaskGutter | undefined } = {};
  private subscriptions: Disposable[] = [];
  @@ -104,19 +97,8 @@ export class LeanTaskGutter implements Disposable {
  this.subscriptions.push(
  window.onDidChangeVisibleTextEditors(() => this.updateDecos()),
  client.progressChanged((progress) => {
  - for (const [uri, processing] of progress) {
  - if (processing.length === 0) {
  - this.status[uri.toString()] = undefined
  - } else {
  - const newStatus = new Map<LeanFileProgressKind, number>()
  - for (const kind of this.decorations.keys()) {
  - const kindProcessing = processing.filter(p => (p.kind === undefined ? LeanFileProgressKind.Processing : p.kind) === kind)
  - if (kindProcessing.length > 0) {
  - newStatus.set(kind, Math.min(...kindProcessing.map(p => p.range.start.line)))
  - }
  - }
  - this.status[uri.toString()] = newStatus
  - }
  + for (const [uri, processed] of progress) {
  + this.status[uri.toString()] = processed
  }
  this.updateDecos()
  }));
  