clarified names;
authorwenzelm
Sat, 25 Oct 2025 19:14:51 +0200
changeset 83385 669b11a039bc
parent 83384 81a832cab4e2
child 83386 5294055465d3
clarified names;
src/Tools/VSCode/extension/media/documentation.js
src/Tools/VSCode/extension/src/documentation_panel.ts
--- 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 () {
--- 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);
       }
     });