src/Tools/VSCode/extension/media/documentation.js
changeset 83363 486e094b676c
child 83385 669b11a039bc
equal deleted inserted replaced
83344:3de18e94ac7c 83363:486e094b676c
       
     1 (function () {
       
     2     const vscode = acquireVsCodeApi();
       
     3   
       
     4     window.addEventListener("message", event => {
       
     5       const message = event.data;
       
     6   
       
     7       if (message.command === "update" && Array.isArray(message.sections)) {
       
     8         renderDocumentation(message.sections);
       
     9       }
       
    10     });
       
    11   
       
    12     function renderDocumentation(sections) {
       
    13       const container = document.getElementById("documentation-container");
       
    14       if (!container) return;
       
    15       container.innerHTML = "";
       
    16 
       
    17       vscode.setState({ sections: sections });
       
    18   
       
    19       const list = document.createElement("ul");
       
    20       list.classList.add("doc-list");
       
    21   
       
    22       let selectedEntry = null;
       
    23   
       
    24       sections.forEach(section => {
       
    25         const sectionItem = document.createElement("li");
       
    26         sectionItem.classList.add("doc-section");
       
    27   
       
    28         const titleElement = document.createElement("span");
       
    29         titleElement.textContent = section.title;
       
    30         titleElement.classList.add("section-title");
       
    31   
       
    32         const subList = document.createElement("ul");
       
    33         subList.classList.add("doc-sublist");
       
    34         subList.style.display = section.important ? "block" : "none";
       
    35   
       
    36         titleElement.addEventListener("click", () => {
       
    37           subList.style.display = subList.style.display === "none" ? "block" : "none";
       
    38         });
       
    39   
       
    40         section.entries.forEach(entry => {
       
    41           const entryItem = document.createElement("li");
       
    42           entryItem.classList.add("doc-entry");
       
    43   
       
    44           let cleanedPath = entry.path.replace(/["]/g, "");
       
    45           if (section.title.includes("Examples")) {
       
    46             cleanedPath = cleanedPath.replace(/^.*?src\//, "src/");
       
    47           }
       
    48           if (section.title.includes("Release Notes")) {
       
    49             cleanedPath = cleanedPath.replace(/^\$ISABELLE_HOME\//, "");
       
    50           }
       
    51   
       
    52           let displayText = cleanedPath;
       
    53           const match = cleanedPath.match(/([^\/]+?)(?:\.pdf)?$/);
       
    54           if (match) {
       
    55             const filename = match[1];
       
    56             const cleanTitle = entry.title.replace(/["']/g, "").trim();
       
    57             displayText = `<b>${filename}</b>${cleanTitle ? ': ' + cleanTitle : ''}`;
       
    58           }
       
    59   
       
    60           const entryLink = document.createElement("a");
       
    61           entryLink.innerHTML = displayText;
       
    62           entryLink.href = "#";
       
    63           entryLink.classList.add("doc-link");
       
    64   
       
    65           entryLink.addEventListener("click", event => {
       
    66             event.preventDefault();
       
    67   
       
    68             if (selectedEntry && selectedEntry !== entryItem) {
       
    69               selectedEntry.classList.remove("selected");
       
    70             }
       
    71   
       
    72             if (selectedEntry === entryItem) {
       
    73               selectedEntry.classList.remove("selected");
       
    74               selectedEntry = null;
       
    75             } else {
       
    76               selectedEntry = entryItem;
       
    77               entryItem.classList.add("selected");
       
    78               openFile(entry.path);
       
    79             }
       
    80           });
       
    81   
       
    82           entryItem.appendChild(entryLink);
       
    83           subList.appendChild(entryItem);
       
    84         });
       
    85   
       
    86         sectionItem.appendChild(titleElement);
       
    87         sectionItem.appendChild(subList);
       
    88         list.appendChild(sectionItem);
       
    89       });
       
    90   
       
    91       container.appendChild(list);
       
    92     }
       
    93   
       
    94     function openFile(filePath) {
       
    95       vscode.postMessage({ command: "openFile", path: filePath });
       
    96     }
       
    97   
       
    98     window.onload = function () {
       
    99         const savedState = vscode.getState();
       
   100         if (savedState && savedState.sections) {
       
   101           renderDocumentation(savedState.sections);
       
   102         }
       
   103       };
       
   104   })();
       
   105