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