# HG changeset patch
# User Thomas Lindae <thomas.lindae@in.tum.de>
# Date 1716808709 -7200
# Node ID 6206f3b2625ab2814d5e87f760fec3bdfd7f5ce6
# Parent  2174ec5f0d0c15f0ae91f20c476a137157170b32
vscode: added decoration request on file switch;

diff -r 2174ec5f0d0c -r 6206f3b2625a src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Mon May 27 13:17:09 2024 +0200
+++ b/src/Tools/VSCode/extension/src/extension.ts	Mon May 27 13:18:29 2024 +0200
@@ -140,6 +140,23 @@
     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()
diff -r 2174ec5f0d0c -r 6206f3b2625a src/Tools/VSCode/extension/src/lsp.ts
--- a/src/Tools/VSCode/extension/src/lsp.ts	Mon May 27 13:17:09 2024 +0200
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Mon May 27 13:18:29 2024 +0200
@@ -32,6 +32,15 @@
   new NotificationType<Document_Decorations>("PIDE/decoration")
 
 
+export interface Decoration_Request
+{
+  uri: string
+}
+
+export const decoration_request_type =
+  new NotificationType<Decoration_Request>("PIDE/decoration_request")
+
+
 /* caret handling */
 
 export interface Caret_Update