src/Tools/VSCode/extension/media/documentation.js
changeset 83385 669b11a039bc
parent 83363 486e094b676c
child 83386 5294055465d3
equal deleted inserted replaced
83384:81a832cab4e2 83385:669b11a039bc
    73               selectedEntry.classList.remove("selected");
    73               selectedEntry.classList.remove("selected");
    74               selectedEntry = null;
    74               selectedEntry = null;
    75             } else {
    75             } else {
    76               selectedEntry = entryItem;
    76               selectedEntry = entryItem;
    77               entryItem.classList.add("selected");
    77               entryItem.classList.add("selected");
    78               openFile(entry.path);
    78               open_document(entry.path);
    79             }
    79             }
    80           });
    80           });
    81   
    81   
    82           entryItem.appendChild(entryLink);
    82           entryItem.appendChild(entryLink);
    83           subList.appendChild(entryItem);
    83           subList.appendChild(entryItem);
    89       });
    89       });
    90   
    90   
    91       container.appendChild(list);
    91       container.appendChild(list);
    92     }
    92     }
    93   
    93   
    94     function openFile(filePath) {
    94     function open_document(path) {
    95       vscode.postMessage({ command: "openFile", path: filePath });
    95       vscode.postMessage({ command: "open_document", path: path });
    96     }
    96     }
    97   
    97   
    98     window.onload = function () {
    98     window.onload = function () {
    99         const savedState = vscode.getState();
    99         const savedState = vscode.getState();
   100         if (savedState && savedState.sections) {
   100         if (savedState && savedState.sections) {