src/Tools/VSCode/extension/media/documentation.js
author paulson <lp15@cam.ac.uk>
Thu, 06 Nov 2025 10:55:39 +0000
changeset 83520 6f656fc94319
parent 83390 05abe5a82410
permissions -rw-r--r--
NEWS
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;
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
     6
      if (message.command === "update" && Array.isArray(message.sections)) {
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
     7
        update(message.sections);
83363
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
     8
      }
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
     9
    });
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    10
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    11
    function update(sections) {
83363
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    12
      const container = document.getElementById("documentation-container");
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    13
      if (!container) return;
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    14
      container.innerHTML = "";
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    15
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    16
      vscode.setState({ sections: sections });
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    17
83363
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    18
      const list = document.createElement("ul");
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    19
      list.classList.add("doc-list");
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    20
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    21
      let selected_entry = null;
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    22
83363
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    23
      sections.forEach(section => {
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    24
        const section_item = document.createElement("li");
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    25
        section_item.classList.add("doc-section");
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    26
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    27
        const title_element = document.createElement("span");
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    28
        title_element.textContent = section.title;
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    29
        title_element.classList.add("section-title");
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    30
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    31
        const sub_list = document.createElement("ul");
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    32
        sub_list.classList.add("doc-sublist");
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    33
        sub_list.style.display = section.important ? "block" : "none";
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    34
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    35
        title_element.addEventListener("click", () => {
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    36
          sub_list.style.display = sub_list.style.display === "none" ? "block" : "none";
83363
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    37
        });
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    38
83363
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    39
        section.entries.forEach(entry => {
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    40
          const entry_item = document.createElement("li");
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    41
          entry_item.classList.add("doc-entry");
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    42
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    43
          const entry_link = document.createElement("a");
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    44
          entry_link.innerHTML = entry.print_html;
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    45
          entry_link.href = "#";
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    46
          entry_link.classList.add("doc-link");
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    47
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    48
          entry_link.addEventListener("click", event => {
83363
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    49
            event.preventDefault();
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    50
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    51
            if (selected_entry && selected_entry !== entry_item) {
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    52
              selected_entry.classList.remove("selected");
83363
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    53
            }
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    54
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    55
            if (selected_entry === entry_item) {
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    56
              selected_entry.classList.remove("selected");
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    57
              selected_entry = null;
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    58
            }
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    59
            else {
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    60
              selected_entry = entry_item;
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    61
              entry_item.classList.add("selected");
83388
8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path;
wenzelm
parents: 83386
diff changeset
    62
              open_document(entry.platform_path);
83363
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    63
            }
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    64
          });
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    65
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    66
          entry_item.appendChild(entry_link);
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    67
          sub_list.appendChild(entry_item);
83363
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    68
        });
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    69
83389
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    70
        section_item.appendChild(title_element);
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    71
        section_item.appendChild(sub_list);
8d9c494b78cf tuned names: avoid camel-case;
wenzelm
parents: 83388
diff changeset
    72
        list.appendChild(section_item);
83363
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    73
      });
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    74
83363
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    75
      container.appendChild(list);
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    76
    }
83386
5294055465d3 tuned whitespace;
wenzelm
parents: 83385
diff changeset
    77
83388
8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path;
wenzelm
parents: 83386
diff changeset
    78
    function open_document(platform_path) {
8d90bd0e4f39 more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path;
wenzelm
parents: 83386
diff changeset
    79
      vscode.postMessage({ command: "open_document", platform_path: platform_path });
83363
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
    window.onload = function () {
83390
05abe5a82410 tuned whitespace;
wenzelm
parents: 83389
diff changeset
    83
      const state = vscode.getState();
05abe5a82410 tuned whitespace;
wenzelm
parents: 83389
diff changeset
    84
      if (state && state.sections) {
05abe5a82410 tuned whitespace;
wenzelm
parents: 83389
diff changeset
    85
        update(state.sections);
05abe5a82410 tuned whitespace;
wenzelm
parents: 83389
diff changeset
    86
      }
05abe5a82410 tuned whitespace;
wenzelm
parents: 83389
diff changeset
    87
    };
83363
486e094b676c various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff changeset
    88
  })();