--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/media/symbols.js Thu Oct 23 16:15:40 2025 +0200
@@ -0,0 +1,348 @@
+(function () {
+ const vscode = acquireVsCodeApi();
+ let allSymbols = {};
+ let allAbbrevsFromThy = [];
+ let controlSup = "";
+ let controlSub = "";
+
+ function decodeHtmlEntity(code) {
+ try {
+ return String.fromCodePoint(code);
+ } catch (error) {
+ return "?";
+ }
+ }
+
+ function formatGroupName(group) {
+ const groupNameMap = {
+ "Z_Notation": "Z Notation",
+ "Control_Block": "Control Block",
+ "Arrow": "Arrow",
+ "Control": "Control",
+ "Digit": "Digit",
+ "Document": "Document",
+ "Greek": "Greek",
+ "Icon": "Icon",
+ "Letter": "Letter",
+ "Logic": "Logic",
+ "Operator": "Operator",
+ "Punctuation": "Punctuation",
+ "Relation": "Relation",
+ "Unsorted": "Unsorted",
+ "Search": "Search"
+ };
+
+ return groupNameMap[group] || group.replace(/_/g, " ").replace(/\b\w/g, c => c.toUpperCase());
+ }
+
+ function createSearchField() {
+ const searchContainer = document.createElement('div');
+ searchContainer.classList.add('search-container');
+
+ const searchInput = document.createElement('input');
+ searchInput.type = "text";
+ searchInput.classList.add('search-input');
+
+ const searchResults = document.createElement('div');
+ searchResults.classList.add('search-results');
+
+ searchInput.addEventListener('input', () => filterSymbols(searchInput.value, searchResults));
+
+ searchContainer.appendChild(searchInput);
+ searchContainer.appendChild(searchResults);
+ return { searchContainer, searchResults };
+ }
+
+ function filterSymbols(query, resultsContainer) {
+ const normalizedQuery = query.toLowerCase().trim();
+ resultsContainer.innerHTML = '';
+
+ if (normalizedQuery === "") return;
+
+ const matchingSymbols = [];
+ Object.values(allSymbols).forEach(symbolList => {
+ symbolList.forEach(symbol => {
+ if (!symbol.code) return;
+
+ if (
+ symbol.symbol.toLowerCase().includes(normalizedQuery) ||
+ (symbol.abbrevs && symbol.abbrevs.some(abbr => abbr.toLowerCase().includes(normalizedQuery)))
+ ) {
+ matchingSymbols.push(symbol);
+ }
+ });
+ });
+
+ const searchLimit = 50;
+ if (matchingSymbols.length === 0) {
+ resultsContainer.innerHTML = "<p>No symbols found</p>";
+ } else {
+ matchingSymbols.slice(0, searchLimit).forEach(symbol => {
+ const decodedSymbol = decodeHtmlEntity(symbol.code);
+ if (!decodedSymbol) return;
+
+ const button = document.createElement('div');
+ button.classList.add('symbol-button');
+ button.textContent = decodedSymbol;
+ button.setAttribute("data-tooltip", `${symbol.symbol}\nAbbreviations: ${symbol.abbrevs.join(', ')}`);
+
+ button.addEventListener('click', () => {
+ vscode.postMessage({ command: 'insertSymbol', symbol: decodedSymbol });
+ });
+
+ resultsContainer.appendChild(button);
+ });
+
+ if (matchingSymbols.length > searchLimit) {
+ const moreResults = document.createElement('div');
+ moreResults.classList.add('more-results');
+ moreResults.textContent = `(${matchingSymbols.length - searchLimit} more...)`;
+ resultsContainer.appendChild(moreResults);
+ }
+ }
+ }
+
+ function renderWithEffects(symbol) {
+ if (!symbol) return "";
+
+ let result = "";
+ let i = 0;
+ while (i < symbol.length) {
+ const char = symbol[i];
+ if (char === "⇧") {
+ i++;
+ if (i < symbol.length) result += "<sup>" + symbol[i] + "</sup>";
+ } else if (char === "⇩") {
+ i++;
+ if (i < symbol.length) result += "<sub>" + symbol[i] + "</sub>";
+ } else {
+ result += char;
+ }
+ i++;
+ }
+ return result;
+ }
+
+ function convertSymbolWithEffects(symbol) {
+ let result = "";
+ let i = 0;
+ while (i < symbol.length) {
+ const char = symbol[i];
+ if (char === "⇧") {
+ i++;
+ if (i < symbol.length) {
+ if (controlSup) result += controlSup + symbol[i];
+ else result += symbol[i];
+ }
+ } else if (char === "⇩") {
+ i++;
+ if (i < symbol.length) {
+ if (controlSub) result += controlSub + symbol[i];
+ else result += symbol[i];
+ }
+ } else {
+ result += char;
+ }
+ i++;
+ }
+ return result;
+}
+
+ function sanitizeSymbolForInsert(symbol) {
+ return symbol.replace(/\u0007/g, '');
+ }
+
+ function extractControlSymbols(symbolGroups) {
+ if (!symbolGroups || !symbolGroups["control"]) return;
+ symbolGroups["control"].forEach(symbol => {
+ if (symbol.name === "sup") controlSup = String.fromCodePoint(symbol.code);
+ if (symbol.name === "sub") controlSub = String.fromCodePoint(symbol.code);
+ });
+ }
+
+ function renderSymbols(groupedSymbols, abbrevsFromThy) {
+ const container = document.getElementById('symbols-container');
+ container.innerHTML = '';
+
+ allSymbols = groupedSymbols;
+ allAbbrevsFromThy = abbrevsFromThy || [];
+
+ extractControlSymbols(groupedSymbols);
+
+ vscode.setState({ symbols: groupedSymbols, abbrevs_from_Thy: allAbbrevsFromThy });
+
+ if (!groupedSymbols || Object.keys(groupedSymbols).length === 0) {
+ container.innerHTML = "<p>No symbols available.</p>";
+ return;
+ }
+
+ const tabs = document.createElement('div');
+ tabs.classList.add('tabs');
+
+ const content = document.createElement('div');
+ content.classList.add('content');
+
+ Object.keys(groupedSymbols).forEach((group, index) => {
+ const tab = document.createElement('button');
+ tab.classList.add('tab');
+ tab.textContent = formatGroupName(group);
+ if (index === 0) tab.classList.add('active');
+
+ tab.addEventListener('click', () => {
+ document.querySelectorAll('.tab').forEach(t => t.classList.remove('active'));
+ tab.classList.add('active');
+ document.querySelectorAll('.tab-content').forEach(c => c.classList.add('hidden'));
+ document.getElementById(`content-${group}`).classList.remove('hidden');
+ });
+
+ tabs.appendChild(tab);
+
+ const groupContent = document.createElement('div');
+ groupContent.classList.add('tab-content');
+ groupContent.id = `content-${group}`;
+ if (index !== 0) groupContent.classList.add('hidden');
+
+ if (group === "control") {
+ const resetButton = document.createElement('button');
+ resetButton.classList.add('reset-button');
+ resetButton.textContent = "Reset";
+
+
+ resetButton.addEventListener('click', () => {
+ vscode.postMessage({ command: 'resetControlSymbols' });
+ });
+ groupContent.appendChild(resetButton);
+
+ const controlButtons = ["sup", "sub", "bold"];
+ controlButtons.forEach(action => {
+ const controlSymbol = groupedSymbols[group].find(s => s.name === action);
+ if (controlSymbol) {
+ const decodedSymbol = decodeHtmlEntity(controlSymbol.code);
+ const button = document.createElement('button');
+ button.classList.add('control-button');
+ button.textContent = decodedSymbol;
+ button.title = action.charAt(0).toUpperCase() + action.slice(1);
+ button.addEventListener('click', () => {
+ vscode.postMessage({ command: 'applyControl', action: action });
+ });
+ groupContent.appendChild(button);
+ }
+ });
+ }
+
+ groupedSymbols[group].forEach(symbol => {
+ if (!symbol.code) return;
+ if (["sup", "sub", "bold"].includes(symbol.name)) return;
+ const decodedSymbol = decodeHtmlEntity(symbol.code);
+ if (!decodedSymbol) return;
+
+ const button = document.createElement('div');
+ if (group === "arrow") {
+ button.classList.add('arrow-button'); // Spezielle Klasse für Pfeile
+ } else {
+ button.classList.add('symbol-button');
+ }
+ button.textContent = decodedSymbol;
+ button.setAttribute("data-tooltip", `${symbol.symbol}\nAbbreviations: ${symbol.abbrevs.join(', ')}`);
+
+ button.addEventListener('click', () => {
+ vscode.postMessage({ command: 'insertSymbol', symbol: decodedSymbol });
+ });
+
+ groupContent.appendChild(button);
+ });
+
+ content.appendChild(groupContent);
+ });
+
+ const abbrevsTab = document.createElement('button');
+ abbrevsTab.classList.add('tab');
+ abbrevsTab.textContent = "Abbrevs";
+ abbrevsTab.addEventListener('click', () => {
+ document.querySelectorAll('.tab').forEach(t => t.classList.remove('active'));
+ abbrevsTab.classList.add('active');
+ document.querySelectorAll('.tab-content').forEach(c => c.classList.add('hidden'));
+ document.getElementById("abbrevs-tab-content").classList.remove('hidden');
+ });
+ tabs.appendChild(abbrevsTab);
+
+ const abbrevsContent = document.createElement('div');
+ abbrevsContent.classList.add('tab-content', 'hidden');
+ abbrevsContent.id = "abbrevs-tab-content";
+
+ allAbbrevsFromThy
+ .filter(([abbr, symbol]) => symbol && symbol.trim() !== "" && !/^[a-zA-Z0-9 _-]+$/.test(symbol))
+ .forEach(([abbr, symbol]) => {
+ const btn = document.createElement('div');
+ btn.classList.add('abbrevs-button');
+ btn.innerHTML = renderWithEffects(symbol);
+ btn.title = abbr;
+ btn.addEventListener('click', () => {
+ vscode.postMessage({ command: 'insertSymbol', symbol: convertSymbolWithEffects(sanitizeSymbolForInsert(symbol)) });
+ });
+
+ abbrevsContent.appendChild(btn);
+ });
+
+ content.appendChild(abbrevsContent);
+
+ const searchTab = document.createElement('button');
+ searchTab.classList.add('tab');
+ searchTab.textContent = "Search";
+ searchTab.addEventListener('click', () => {
+ document.querySelectorAll('.tab').forEach(t => t.classList.remove('active'));
+ searchTab.classList.add('active');
+ document.querySelectorAll('.tab-content').forEach(c => c.classList.add('hidden'));
+ document.getElementById("search-tab-content").classList.remove('hidden');
+ });
+ tabs.appendChild(searchTab);
+
+ const { searchContainer, searchResults } = createSearchField();
+ const searchContent = document.createElement('div');
+ searchContent.classList.add('tab-content', 'hidden');
+ searchContent.id = "search-tab-content";
+ searchContent.appendChild(searchContainer);
+
+ content.appendChild(searchContent);
+ container.appendChild(tabs);
+ container.appendChild(content);
+
+ const tooltip = document.createElement("div");
+ tooltip.className = "tooltip";
+ document.body.appendChild(tooltip);
+
+ document.querySelectorAll(".symbol-button, .arrow-button, .abbrevs-button").forEach(button => {
+ button.addEventListener("mouseenter", (e) => {
+ const rect = button.getBoundingClientRect();
+ const text = button.getAttribute("data-tooltip");
+
+ if (text) {
+ tooltip.textContent = text;
+ tooltip.style.left = `${rect.left + window.scrollX}px`;
+ tooltip.style.top = `${rect.bottom + 6 + window.scrollY}px`;
+ tooltip.classList.add("visible");
+ }
+ });
+
+ button.addEventListener("mouseleave", () => {
+ tooltip.classList.remove("visible");
+ tooltip.textContent = "";
+ });
+ });
+
+ }
+
+ window.addEventListener('message', event => {
+ if (event.data.command === 'update' && event.data.symbols) {
+ renderSymbols(event.data.symbols, event.data.abbrevs_from_Thy);
+ }
+ });
+
+ window.onload = function () {
+ const savedState = vscode.getState();
+ if (savedState && savedState.symbols) {
+ renderSymbols(savedState.symbols, savedState.abbrevs_from_Thy);
+ }
+ };
+
+})();