# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1720178105 -7200
# Node ID de30087b4ff86afb5dcbdfeb48bd6dfc190ebae3
# Parent  54bda6e0e848f0c4c80860f7e93b605b10f9de60
vscode: switched document_decoration map to use strings as keys instead of Uris, because Uri equality check is inconsistent;
disabled decoration requests as decoration caching is already done on client-side;

diff -r 54bda6e0e848 -r de30087b4ff8 src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Mon Jul 01 04:34:04 2024 +0200
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Fri Jul 05 13:15:05 2024 +0200
@@ -164,11 +164,11 @@
 /* decoration for document node */
 
 type Content = Range[] | DecorationOptions[]
-const document_decorations = new Map<Uri, Map<string, Content>>()
+const document_decorations = new Map<string, Map<string, Content>>()
 
 export function close_document(document: TextDocument)
 {
-  document_decorations.delete(document.uri)
+  document_decorations.delete(document.uri.toString())
 }
 
 export function apply_decoration(decorations: Document_Decorations)
@@ -187,9 +187,9 @@
           }
         })
 
-      const document = document_decorations.get(uri) || new Map<string, Content>()
+      const document = document_decorations.get(uri.toString()) || new Map<string, Content>()
       document.set(decoration.type, content)
-      document_decorations.set(uri, document)
+      document_decorations.set(uri.toString(), document)
 
       for (const editor of window.visibleTextEditors) {
         if (uri.toString === editor.document.uri.toString) {
@@ -203,7 +203,7 @@
 export function update_editor(editor: TextEditor)
 {
   if (editor) {
-    const decorations = document_decorations.get(editor.document.uri)
+    const decorations = document_decorations.get(editor.document.uri.toString())
     if (decorations) {
       for (const [typ, content] of decorations) {
         editor.setDecorations(types.get(typ), content)
diff -r 54bda6e0e848 -r de30087b4ff8 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Mon Jul 01 04:34:04 2024 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Fri Jul 05 13:15:05 2024 +0200
@@ -146,23 +146,6 @@
     register_script_decorations(context)
 
 
-    /* manual decorations */
-
-    function request_decs()
-    {
-      const document_uri = window.activeTextEditor.document.uri
-      const decoration_request: lsp.Decoration_Request = { uri: document_uri.toString() }
-      language_client.sendNotification(lsp.decoration_request_type, decoration_request)
-    }
-
-    language_client.onReady().then(() =>
-    {
-      context.subscriptions.push(
-        window.onDidChangeActiveTextEditor(request_decs)
-      )
-    })
-
-
     /* caret handling */
 
     function update_caret()