src/Tools/VSCode/extension/media/symbols.js

various improvements of Isabelle/VSCode: original changeset by Diana Korchmar, LMU München;

(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);
    }
  };

})();