# HG changeset patch
# User wenzelm
# Date 1761412491 -7200
# Node ID 669b11a039bc03ed96766f272b5c0814a20a9592
# Parent  81a832cab4e286dffcd0e5def44815ee7b67382e
clarified names;

diff -r 81a832cab4e2 -r 669b11a039bc src/Tools/VSCode/extension/media/documentation.js
--- a/src/Tools/VSCode/extension/media/documentation.js	Sat Oct 25 19:05:32 2025 +0200
+++ b/src/Tools/VSCode/extension/media/documentation.js	Sat Oct 25 19:14:51 2025 +0200
@@ -75,7 +75,7 @@
             } else {
               selectedEntry = entryItem;
               entryItem.classList.add("selected");
-              openFile(entry.path);
+              open_document(entry.path);
             }
           });
   
@@ -91,8 +91,8 @@
       container.appendChild(list);
     }
   
-    function openFile(filePath) {
-      vscode.postMessage({ command: "openFile", path: filePath });
+    function open_document(path) {
+      vscode.postMessage({ command: "open_document", path: path });
     }
   
     window.onload = function () {
diff -r 81a832cab4e2 -r 669b11a039bc src/Tools/VSCode/extension/src/documentation_panel.ts
--- a/src/Tools/VSCode/extension/src/documentation_panel.ts	Sat Oct 25 19:05:32 2025 +0200
+++ b/src/Tools/VSCode/extension/src/documentation_panel.ts	Sat Oct 25 19:14:51 2025 +0200
@@ -67,7 +67,7 @@
     }
 
     this._view.webview.onDidReceiveMessage(async message => {
-      if (message.command === 'openFile') {
+      if (message.command === 'open_document') {
         this._open_document(message.path);
       }
     });