# HG changeset patch
# User wenzelm
# Date 1582727893 -3600
# Node ID bb1c829534ba4d55668a2f761655e2044eed0e45
# Parent  6aa2dc2639127a4d00e1e59b602f89b438949a11
obsolete;

diff -r 6aa2dc263912 -r bb1c829534ba src/Tools/VSCode/extension/src/content_provider.ts
--- a/src/Tools/VSCode/extension/src/content_provider.ts	Wed Feb 26 15:38:04 2020 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-'use strict'
-
-import { Event, EventEmitter, Uri, TextDocumentContentProvider, Disposable,
-  workspace } from 'vscode'
-
-
-export class Content_Provider implements TextDocumentContentProvider
-{
-  private _uri_template: Uri
-  get uri_template(): Uri { return this._uri_template }
-  get uri_scheme(): string { return this.uri_template.scheme }
-
-  constructor(uri_scheme: string)
-  {
-    this._uri_template = Uri.parse("scheme:").with({ scheme: uri_scheme })
-  }
-  dispose() { }
-
-  private emitter = new EventEmitter<Uri>()
-  public update(uri: Uri) { this.emitter.fire(uri) }
-  get onDidChange(): Event<Uri> { return this.emitter.event }
-
-  private content = new Map<string, string>()
-  public set_content(uri: Uri, content: string) { this.content.set(uri.toString(), content)}
-
-  provideTextDocumentContent(uri: Uri): string
-  {
-    return this.content.get(uri.toString()) || ""
-  }
-
-  public register(): Disposable
-  {
-    return workspace.registerTextDocumentContentProvider(this.uri_scheme, this)
-  }
-}