39 |
39 |
40 section.entries.forEach(entry => { |
40 section.entries.forEach(entry => { |
41 const entryItem = document.createElement("li"); |
41 const entryItem = document.createElement("li"); |
42 entryItem.classList.add("doc-entry"); |
42 entryItem.classList.add("doc-entry"); |
43 |
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"); |
44 const entryLink = document.createElement("a"); |
61 entryLink.innerHTML = displayText; |
45 entryLink.innerHTML = entry.print_html; |
62 entryLink.href = "#"; |
46 entryLink.href = "#"; |
63 entryLink.classList.add("doc-link"); |
47 entryLink.classList.add("doc-link"); |
64 |
48 |
65 entryLink.addEventListener("click", event => { |
49 entryLink.addEventListener("click", event => { |
66 event.preventDefault(); |
50 event.preventDefault(); |
73 selectedEntry.classList.remove("selected"); |
57 selectedEntry.classList.remove("selected"); |
74 selectedEntry = null; |
58 selectedEntry = null; |
75 } else { |
59 } else { |
76 selectedEntry = entryItem; |
60 selectedEntry = entryItem; |
77 entryItem.classList.add("selected"); |
61 entryItem.classList.add("selected"); |
78 open_document(entry.path); |
62 open_document(entry.platform_path); |
79 } |
63 } |
80 }); |
64 }); |
81 |
65 |
82 entryItem.appendChild(entryLink); |
66 entryItem.appendChild(entryLink); |
83 subList.appendChild(entryItem); |
67 subList.appendChild(entryItem); |
89 }); |
73 }); |
90 |
74 |
91 container.appendChild(list); |
75 container.appendChild(list); |
92 } |
76 } |
93 |
77 |
94 function open_document(path) { |
78 function open_document(platform_path) { |
95 vscode.postMessage({ command: "open_document", path: path }); |
79 vscode.postMessage({ command: "open_document", platform_path: platform_path }); |
96 } |
80 } |
97 |
81 |
98 window.onload = function () { |
82 window.onload = function () { |
99 const savedState = vscode.getState(); |
83 const savedState = vscode.getState(); |
100 if (savedState && savedState.sections) { |
84 if (savedState && savedState.sections) { |