| author | wenzelm |
| Sat, 25 Oct 2025 19:20:37 +0200 | |
| changeset 83386 | 5294055465d3 |
| parent 83385 | 669b11a039bc |
| child 83388 | 8d90bd0e4f39 |
| permissions | -rw-r--r-- |
|
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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 93 |
|
| 83385 | 94 |
function open_document(path) {
|
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 | 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 |
})(); |