message: fix: change usages of LeanFileProgressKind in taskgutter to constants
diff: @@ -2,6 +2,10 @@ import { Disposable, ExtensionContext, OverviewRulerLane, Range, TextEditorDecor
  import { LeanClient } from './leanclient';
  import { LeanFileProgressKind, LeanFileProgressProcessingInfo } from '@lean4/infoview';
  +// Workaround, since LeanFileProgressKind.* gives a 'self is not defined' error
  +const ProgressKind_Processing = 1
  +const ProgressKind_FatalError = 2
  +
  class LeanFileTaskGutter {
  private timeout?: NodeJS.Timeout
  @@ -42,7 +46,7 @@ class LeanFileTaskGutter {
  editor.setDecorations(
  decoration,
  this.processed
  - .filter(info => (info.kind === undefined ? LeanFileProgressKind.Processing : info.kind) === kind)
  + .filter(info => (info.kind === undefined ? ProgressKind_Processing : info.kind) === kind)
  .map(info => ({
  range: new Range(info.range.start.line, 0, info.range.end.line, 0),
  hoverMessage: message
  @@ -65,7 +69,7 @@ export class LeanTaskGutter implements Disposable {
  private subscriptions: Disposable[] = [];
  constructor(client: LeanClient, context: ExtensionContext) {
  - this.decorations.set(LeanFileProgressKind.Processing, [
  + this.decorations.set(ProgressKind_Processing, [
  window.createTextEditorDecorationType({
  overviewRulerLane: OverviewRulerLane.Left,
  overviewRulerColor: 'rgba(255, 165, 0, 0.5)',
  @@ -79,7 +83,7 @@ export class LeanTaskGutter implements Disposable {
  }),
  'busily processing...'
  ])
  - this.decorations.set(LeanFileProgressKind.FatalError, [
  + this.decorations.set(ProgressKind_FatalError, [
  window.createTextEditorDecorationType({
  overviewRulerLane: OverviewRulerLane.Left,
  overviewRulerColor: 'rgba(255, 0, 0, 0.5)',
  