| author | paulson <lp15@cam.ac.uk> |
| Thu, 06 Nov 2025 10:55:39 +0000 | |
| changeset 83520 | 6f656fc94319 |
| parent 83487 | b284ff764c80 |
| 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(); |
| 83461 | 3 |
let all_symbols = {};
|
| 83469 | 4 |
let all_abbrevs = []; |
| 83461 | 5 |
let control_sup = ""; |
6 |
let control_sub = ""; |
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
7 |
|
| 83487 | 8 |
function symbol_tooltip(symbol) {
|
9 |
const res = [symbol.symbol] |
|
10 |
for (const a of symbol.abbrevs) {
|
|
11 |
res.push(`\nabbrev: ${a}`);
|
|
12 |
} |
|
13 |
return res.join("")
|
|
14 |
} |
|
15 |
||
| 83461 | 16 |
function create_search_field() {
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
17 |
const search_container = document.createElement("div");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
18 |
search_container.classList.add("search-container");
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
19 |
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
20 |
const search_input = document.createElement("input");
|
| 83461 | 21 |
search_input.type = "text"; |
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
22 |
search_input.classList.add("search-input");
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
23 |
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
24 |
const search_results = document.createElement("div");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
25 |
search_results.classList.add("search-results");
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
26 |
|
| 83479 | 27 |
search_input.addEventListener("input", () => filter_symbols(search_input.value, search_results));
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
28 |
|
| 83461 | 29 |
search_container.appendChild(search_input); |
30 |
search_container.appendChild(search_results); |
|
31 |
return { search_container, search_results };
|
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
32 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
33 |
|
| 83479 | 34 |
function filter_symbols(query, results_container) {
|
| 83461 | 35 |
const normalized_query = query.toLowerCase().trim(); |
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
36 |
results_container.innerHTML = ""; |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
37 |
|
| 83461 | 38 |
if (normalized_query === "") return; |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
39 |
|
| 83461 | 40 |
const matching_symbols = []; |
| 83479 | 41 |
Object.values(all_symbols).forEach(symbol_list => {
|
42 |
symbol_list.forEach(symbol => {
|
|
43 |
if (symbol.code && |
|
44 |
(symbol.symbol.toLowerCase().includes(normalized_query) || |
|
45 |
(symbol.abbrevs && symbol.abbrevs.some(abbr => abbr.toLowerCase().includes(normalized_query))))) |
|
46 |
{
|
|
| 83461 | 47 |
matching_symbols.push(symbol); |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
48 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
49 |
}); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
50 |
}); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
51 |
|
| 83461 | 52 |
const search_limit = 50; |
53 |
if (matching_symbols.length === 0) {
|
|
54 |
results_container.innerHTML = "<p>No symbols found</p>"; |
|
| 83396 | 55 |
} |
56 |
else {
|
|
| 83461 | 57 |
matching_symbols.slice(0, search_limit).forEach(symbol => {
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
58 |
const button = document.createElement("div");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
59 |
button.classList.add("symbol-button");
|
| 83476 | 60 |
button.textContent = symbol.decoded; |
| 83487 | 61 |
button.setAttribute("data-tooltip", symbol_tooltip(symbol));
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
62 |
button.addEventListener("click", () => {
|
| 83476 | 63 |
vscode.postMessage({ command: "insert_symbol", symbol: symbol.decoded });
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
64 |
}); |
| 83461 | 65 |
results_container.appendChild(button); |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
66 |
}); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
67 |
|
| 83461 | 68 |
if (matching_symbols.length > search_limit) {
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
69 |
const more_results = document.createElement("div");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
70 |
more_results.classList.add("more-results");
|
| 83461 | 71 |
more_results.textContent = `(${matching_symbols.length - search_limit} more...)`;
|
72 |
results_container.appendChild(more_results); |
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
73 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
74 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
75 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
76 |
|
| 83461 | 77 |
function render_with_effects(symbol) {
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
78 |
if (!symbol) return ""; |
|
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 |
let result = ""; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
81 |
let i = 0; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
82 |
while (i < symbol.length) {
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
83 |
const char = symbol[i]; |
|
83369
8696fb442049
avoid literal Unicode symbols, which are in danger of being recoded;
wenzelm
parents:
83368
diff
changeset
|
84 |
if (char === "\u21e7") {
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
85 |
i++; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
86 |
if (i < symbol.length) result += "<sup>" + symbol[i] + "</sup>"; |
| 83396 | 87 |
} |
88 |
else if (char === "\u21e9") {
|
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
89 |
i++; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
90 |
if (i < symbol.length) result += "<sub>" + symbol[i] + "</sub>"; |
| 83396 | 91 |
} |
92 |
else {
|
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
93 |
result += char; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
94 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
95 |
i++; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
96 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
97 |
return result; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
98 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
99 |
|
| 83461 | 100 |
function convert_symbol_with_effects(symbol) {
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
101 |
let result = ""; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
102 |
let i = 0; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
103 |
while (i < symbol.length) {
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
104 |
const char = symbol[i]; |
|
83369
8696fb442049
avoid literal Unicode symbols, which are in danger of being recoded;
wenzelm
parents:
83368
diff
changeset
|
105 |
if (char === "\u21e7") {
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
106 |
i++; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
107 |
if (i < symbol.length) {
|
| 83461 | 108 |
if (control_sup) result += control_sup + symbol[i]; |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
109 |
else result += symbol[i]; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
110 |
} |
| 83396 | 111 |
} |
112 |
else if (char === "\u21e9") {
|
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
113 |
i++; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
114 |
if (i < symbol.length) {
|
| 83461 | 115 |
if (control_sub) result += control_sub + symbol[i]; |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
116 |
else result += symbol[i]; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
117 |
} |
| 83396 | 118 |
} |
119 |
else {
|
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
120 |
result += char; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
121 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
122 |
i++; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
123 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
124 |
return result; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
125 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
126 |
|
| 83461 | 127 |
function sanitize_symbol_for_insert(symbol) {
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
128 |
return symbol.replace(/\u0007/g, ""); |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
129 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
130 |
|
| 83461 | 131 |
function extract_control_symbols(symbol_groups) {
|
132 |
if (!symbol_groups || !symbol_groups["control"]) return; |
|
133 |
symbol_groups["control"].forEach(symbol => {
|
|
134 |
if (symbol.name === "sup") control_sup = String.fromCodePoint(symbol.code); |
|
135 |
if (symbol.name === "sub") control_sub = String.fromCodePoint(symbol.code); |
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
136 |
}); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
137 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
138 |
|
| 83469 | 139 |
function render_symbols(grouped_symbols, abbrevs) {
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
140 |
const container = document.getElementById("symbols-container");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
141 |
container.innerHTML = ""; |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
142 |
|
| 83461 | 143 |
all_symbols = grouped_symbols; |
| 83469 | 144 |
all_abbrevs = abbrevs || []; |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
145 |
|
| 83461 | 146 |
extract_control_symbols(grouped_symbols); |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
147 |
|
| 83469 | 148 |
vscode.setState({ symbols: grouped_symbols, all_abbrevs });
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
149 |
|
| 83461 | 150 |
if (!grouped_symbols || Object.keys(grouped_symbols).length === 0) {
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
151 |
container.innerHTML = "<p>No symbols available.</p>"; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
152 |
return; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
153 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
154 |
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
155 |
const tabs = document.createElement("div");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
156 |
tabs.classList.add("tabs");
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
157 |
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
158 |
const content = document.createElement("div");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
159 |
content.classList.add("content");
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
160 |
|
| 83485 | 161 |
const abbrevs_tab = document.createElement("button");
|
162 |
abbrevs_tab.classList.add("tab");
|
|
163 |
abbrevs_tab.textContent = "Abbrevs"; |
|
164 |
abbrevs_tab.addEventListener("click", () => {
|
|
165 |
document.querySelectorAll(".tab").forEach(t => t.classList.remove("active"));
|
|
166 |
abbrevs_tab.classList.add("active");
|
|
167 |
document.querySelectorAll(".tab-content").forEach(c => c.classList.add("hidden"));
|
|
168 |
document.getElementById("abbrevs-tab-content").classList.remove("hidden");
|
|
169 |
}); |
|
170 |
tabs.appendChild(abbrevs_tab); |
|
171 |
||
172 |
const abbrevs_content = document.createElement("div");
|
|
173 |
abbrevs_content.classList.add("tab-content", "hidden");
|
|
174 |
abbrevs_content.id = "abbrevs-tab-content"; |
|
175 |
||
176 |
all_abbrevs |
|
177 |
.filter(([abbr, symbol]) => symbol && symbol.trim() !== "" && !/^[a-zA-Z0-9 _-]+$/.test(symbol)) |
|
178 |
.forEach(([abbr, symbol]) => {
|
|
179 |
const btn = document.createElement("div");
|
|
180 |
btn.classList.add("abbrevs-button");
|
|
181 |
btn.innerHTML = render_with_effects(symbol); |
|
182 |
btn.title = abbr; |
|
183 |
btn.addEventListener("click", () => {
|
|
184 |
vscode.postMessage({ command: "insert_symbol", symbol: convert_symbol_with_effects(sanitize_symbol_for_insert(symbol)) });
|
|
185 |
}); |
|
186 |
||
187 |
abbrevs_content.appendChild(btn); |
|
188 |
}); |
|
189 |
||
190 |
content.appendChild(abbrevs_content); |
|
191 |
||
| 83486 | 192 |
Object.keys(grouped_symbols).sort().forEach((group, index) => {
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
193 |
const tab = document.createElement("button");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
194 |
tab.classList.add("tab");
|
|
83473
66134b2d3928
eliminate hardwired data, which is actually not required here;
wenzelm
parents:
83469
diff
changeset
|
195 |
tab.textContent = group.replace(/_/g, " ").replace(/\b\w/g, c => c.toUpperCase()); |
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
196 |
if (index === 0) tab.classList.add("active");
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
197 |
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
198 |
tab.addEventListener("click", () => {
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
199 |
document.querySelectorAll(".tab").forEach(t => t.classList.remove("active"));
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
200 |
tab.classList.add("active");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
201 |
document.querySelectorAll(".tab-content").forEach(c => c.classList.add("hidden"));
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
202 |
document.getElementById(`content-${group}`).classList.remove("hidden");
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
203 |
}); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
204 |
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
205 |
tabs.appendChild(tab); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
206 |
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
207 |
const group_content = document.createElement("div");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
208 |
group_content.classList.add("tab-content");
|
| 83461 | 209 |
group_content.id = `content-${group}`;
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
210 |
if (index !== 0) group_content.classList.add("hidden");
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
211 |
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
212 |
if (group === "control") {
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
213 |
const reset_button = document.createElement("button");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
214 |
reset_button.classList.add("reset-button");
|
| 83461 | 215 |
reset_button.textContent = "Reset"; |
| 83482 | 216 |
reset_button.addEventListener("click", () => vscode.postMessage({ command: "reset_control" }));
|
| 83461 | 217 |
group_content.appendChild(reset_button); |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
218 |
|
| 83461 | 219 |
const control_buttons = ["sup", "sub", "bold"]; |
220 |
control_buttons.forEach(action => {
|
|
221 |
const control_symbol = grouped_symbols[group].find(s => s.name === action); |
|
222 |
if (control_symbol) {
|
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
223 |
const button = document.createElement("button");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
224 |
button.classList.add("control-button");
|
| 83476 | 225 |
button.textContent = control_symbol.decoded; |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
226 |
button.title = action.charAt(0).toUpperCase() + action.slice(1); |
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
227 |
button.addEventListener("click", () => {
|
| 83466 | 228 |
vscode.postMessage({ command: "apply_control", action: action });
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
229 |
}); |
| 83461 | 230 |
group_content.appendChild(button); |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
231 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
232 |
}); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
233 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
234 |
|
| 83461 | 235 |
grouped_symbols[group].forEach(symbol => {
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
236 |
if (!symbol.code) return; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
237 |
if (["sup", "sub", "bold"].includes(symbol.name)) return; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
238 |
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
239 |
const button = document.createElement("div");
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
240 |
if (group === "arrow") {
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
241 |
button.classList.add("arrow-button"); // special class for arrows
|
| 83396 | 242 |
} |
243 |
else {
|
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
244 |
button.classList.add("symbol-button");
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
245 |
} |
| 83476 | 246 |
button.textContent = symbol.decoded; |
| 83487 | 247 |
button.setAttribute("data-tooltip", symbol_tooltip(symbol));
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
248 |
button.addEventListener("click", () => {
|
| 83476 | 249 |
vscode.postMessage({ command: "insert_symbol", symbol: symbol.decoded });
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
250 |
}); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
251 |
|
| 83461 | 252 |
group_content.appendChild(button); |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
253 |
}); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
254 |
|
| 83461 | 255 |
content.appendChild(group_content); |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
256 |
}); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
257 |
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
258 |
const search_tab = document.createElement("button");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
259 |
search_tab.classList.add("tab");
|
| 83461 | 260 |
search_tab.textContent = "Search"; |
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
261 |
search_tab.addEventListener("click", () => {
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
262 |
document.querySelectorAll(".tab").forEach(t => t.classList.remove("active"));
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
263 |
search_tab.classList.add("active");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
264 |
document.querySelectorAll(".tab-content").forEach(c => c.classList.add("hidden"));
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
265 |
document.getElementById("search-tab-content").classList.remove("hidden");
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
266 |
}); |
| 83461 | 267 |
tabs.appendChild(search_tab); |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
268 |
|
| 83461 | 269 |
const { search_container, search_results } = create_search_field();
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
270 |
const search_content = document.createElement("div");
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
271 |
search_content.classList.add("tab-content", "hidden");
|
| 83461 | 272 |
search_content.id = "search-tab-content"; |
273 |
search_content.appendChild(search_container); |
|
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
274 |
|
| 83461 | 275 |
content.appendChild(search_content); |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
276 |
container.appendChild(tabs); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
277 |
container.appendChild(content); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
278 |
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
279 |
const tooltip = document.createElement("div");
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
280 |
tooltip.className = "tooltip"; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
281 |
document.body.appendChild(tooltip); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
282 |
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
283 |
document.querySelectorAll(".symbol-button, .arrow-button, .abbrevs-button").forEach(button => {
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
284 |
button.addEventListener("mouseenter", (e) => {
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
285 |
const rect = button.getBoundingClientRect(); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
286 |
const text = button.getAttribute("data-tooltip");
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
287 |
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
288 |
if (text) {
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
289 |
tooltip.textContent = text; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
290 |
tooltip.style.left = `${rect.left + window.scrollX}px`;
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
291 |
tooltip.style.top = `${rect.bottom + 6 + window.scrollY}px`;
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
292 |
tooltip.classList.add("visible");
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
293 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
294 |
}); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
295 |
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
296 |
button.addEventListener("mouseleave", () => {
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
297 |
tooltip.classList.remove("visible");
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
298 |
tooltip.textContent = ""; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
299 |
}); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
300 |
}); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
301 |
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
302 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
303 |
|
|
83465
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
304 |
window.addEventListener("message", event => {
|
|
4023a9c7070f
tuned quotes: follow Isabelle majority style, instead of JS/TS;
wenzelm
parents:
83461
diff
changeset
|
305 |
if (event.data.command === "update" && event.data.symbols) {
|
| 83469 | 306 |
render_symbols(event.data.symbols, event.data.abbrevs); |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
307 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
308 |
}); |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
309 |
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
310 |
window.onload = function () {
|
| 83461 | 311 |
const state = vscode.getState(); |
312 |
if (state && state.symbols) {
|
|
| 83469 | 313 |
render_symbols(state.symbols, state.abbrevs); |
|
83363
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
314 |
} |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
315 |
}; |
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
316 |
|
|
486e094b676c
various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;
wenzelm
parents:
diff
changeset
|
317 |
})(); |