src/Tools/VSCode/extension/media/symbols.js
author paulson <lp15@cam.ac.uk>
Thu, 06 Nov 2025 10:55:39 +0000
changeset 83520 6f656fc94319
parent 83487 b284ff764c80
permissions -rw-r--r--
NEWS
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
     3
  let all_symbols = {};
83469
53fa51e38c20 clarified names: avoid camel-case;
wenzelm
parents: 83466
diff changeset
     4
  let all_abbrevs = [];
83461
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
     5
  let control_sup = "";
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
     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
b284ff764c80 clarified tooltip, following Isabelle/jEdit;
wenzelm
parents: 83486
diff changeset
     8
  function symbol_tooltip(symbol) {
b284ff764c80 clarified tooltip, following Isabelle/jEdit;
wenzelm
parents: 83486
diff changeset
     9
    const res = [symbol.symbol]
b284ff764c80 clarified tooltip, following Isabelle/jEdit;
wenzelm
parents: 83486
diff changeset
    10
    for (const a of symbol.abbrevs) {
b284ff764c80 clarified tooltip, following Isabelle/jEdit;
wenzelm
parents: 83486
diff changeset
    11
      res.push(`\nabbrev: ${a}`);
b284ff764c80 clarified tooltip, following Isabelle/jEdit;
wenzelm
parents: 83486
diff changeset
    12
    }
b284ff764c80 clarified tooltip, following Isabelle/jEdit;
wenzelm
parents: 83486
diff changeset
    13
    return res.join("")
b284ff764c80 clarified tooltip, following Isabelle/jEdit;
wenzelm
parents: 83486
diff changeset
    14
  }
b284ff764c80 clarified tooltip, following Isabelle/jEdit;
wenzelm
parents: 83486
diff changeset
    15
83461
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    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
436c1a7ae254 tuned: avoid camel-case;
wenzelm
parents: 83476
diff changeset
    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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    29
    search_container.appendChild(search_input);
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    30
    search_container.appendChild(search_results);
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    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
436c1a7ae254 tuned: avoid camel-case;
wenzelm
parents: 83476
diff changeset
    34
  function filter_symbols(query, results_container) {
83461
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    40
    const matching_symbols = [];
83479
436c1a7ae254 tuned: avoid camel-case;
wenzelm
parents: 83476
diff changeset
    41
    Object.values(all_symbols).forEach(symbol_list => {
436c1a7ae254 tuned: avoid camel-case;
wenzelm
parents: 83476
diff changeset
    42
      symbol_list.forEach(symbol => {
436c1a7ae254 tuned: avoid camel-case;
wenzelm
parents: 83476
diff changeset
    43
        if (symbol.code &&
436c1a7ae254 tuned: avoid camel-case;
wenzelm
parents: 83476
diff changeset
    44
          (symbol.symbol.toLowerCase().includes(normalized_query) ||
436c1a7ae254 tuned: avoid camel-case;
wenzelm
parents: 83476
diff changeset
    45
            (symbol.abbrevs && symbol.abbrevs.some(abbr => abbr.toLowerCase().includes(normalized_query)))))
436c1a7ae254 tuned: avoid camel-case;
wenzelm
parents: 83476
diff changeset
    46
        {
83461
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    52
    const search_limit = 50;
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    53
    if (matching_symbols.length === 0) {
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    54
      results_container.innerHTML = "<p>No symbols found</p>";
83396
1cc5bab55049 tuned whitespace;
wenzelm
parents: 83369
diff changeset
    55
    }
1cc5bab55049 tuned whitespace;
wenzelm
parents: 83369
diff changeset
    56
    else {
83461
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    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
fb39900f0a0f eliminate redundant function;
wenzelm
parents: 83473
diff changeset
    60
        button.textContent = symbol.decoded;
83487
b284ff764c80 clarified tooltip, following Isabelle/jEdit;
wenzelm
parents: 83486
diff changeset
    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
fb39900f0a0f eliminate redundant function;
wenzelm
parents: 83473
diff changeset
    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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    71
        more_results.textContent = `(${matching_symbols.length - search_limit} more...)`;
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
    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
1cc5bab55049 tuned whitespace;
wenzelm
parents: 83369
diff changeset
    87
      }
1cc5bab55049 tuned whitespace;
wenzelm
parents: 83369
diff changeset
    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
1cc5bab55049 tuned whitespace;
wenzelm
parents: 83369
diff changeset
    91
      }
1cc5bab55049 tuned whitespace;
wenzelm
parents: 83369
diff changeset
    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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
1cc5bab55049 tuned whitespace;
wenzelm
parents: 83369
diff changeset
   111
    }
1cc5bab55049 tuned whitespace;
wenzelm
parents: 83369
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
1cc5bab55049 tuned whitespace;
wenzelm
parents: 83369
diff changeset
   118
    }
1cc5bab55049 tuned whitespace;
wenzelm
parents: 83369
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   131
  function extract_control_symbols(symbol_groups) {
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   132
    if (!symbol_groups || !symbol_groups["control"]) return;
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   133
    symbol_groups["control"].forEach(symbol => {
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   134
      if (symbol.name === "sup") control_sup = String.fromCodePoint(symbol.code);
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
53fa51e38c20 clarified names: avoid camel-case;
wenzelm
parents: 83466
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   143
    all_symbols = grouped_symbols;
83469
53fa51e38c20 clarified names: avoid camel-case;
wenzelm
parents: 83466
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
53fa51e38c20 clarified names: avoid camel-case;
wenzelm
parents: 83466
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   161
    const abbrevs_tab = document.createElement("button");
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   162
    abbrevs_tab.classList.add("tab");
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   163
    abbrevs_tab.textContent = "Abbrevs";
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   164
    abbrevs_tab.addEventListener("click", () => {
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   165
      document.querySelectorAll(".tab").forEach(t => t.classList.remove("active"));
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   166
      abbrevs_tab.classList.add("active");
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   167
      document.querySelectorAll(".tab-content").forEach(c => c.classList.add("hidden"));
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   168
      document.getElementById("abbrevs-tab-content").classList.remove("hidden");
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   169
    });
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   170
    tabs.appendChild(abbrevs_tab);
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   171
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   172
    const abbrevs_content = document.createElement("div");
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   173
    abbrevs_content.classList.add("tab-content", "hidden");
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   174
    abbrevs_content.id = "abbrevs-tab-content";
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   175
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   176
    all_abbrevs
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   177
      .filter(([abbr, symbol]) => symbol && symbol.trim() !== "" && !/^[a-zA-Z0-9 _-]+$/.test(symbol)) 
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   178
      .forEach(([abbr, symbol]) => {
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   179
        const btn = document.createElement("div");
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   180
        btn.classList.add("abbrevs-button");
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   181
        btn.innerHTML = render_with_effects(symbol); 
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   182
        btn.title = abbr;
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   183
        btn.addEventListener("click", () => {
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   184
          vscode.postMessage({ command: "insert_symbol", symbol: convert_symbol_with_effects(sanitize_symbol_for_insert(symbol)) });
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   185
        });
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   186
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   187
        abbrevs_content.appendChild(btn);
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   188
      });
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   189
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   190
    content.appendChild(abbrevs_content);
b94d2f0133b1 show "Abbrevs" first as in Isabelle/jEdit;
wenzelm
parents: 83482
diff changeset
   191
83486
dcaf9447c083 proper order of groups as in Isabelle/jEdit;
wenzelm
parents: 83485
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   215
        reset_button.textContent = "Reset";
83482
447b52014c0e clarified names;
wenzelm
parents: 83479
diff changeset
   216
        reset_button.addEventListener("click", () => vscode.postMessage({ command: "reset_control" }));
83461
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   219
        const control_buttons = ["sup", "sub", "bold"];
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   220
        control_buttons.forEach(action => {
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   221
          const control_symbol = grouped_symbols[group].find(s => s.name === action);
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
fb39900f0a0f eliminate redundant function;
wenzelm
parents: 83473
diff changeset
   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
4e3eae17917f tuned names: avoid camel-case;
wenzelm
parents: 83465
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
1cc5bab55049 tuned whitespace;
wenzelm
parents: 83369
diff changeset
   242
        }
1cc5bab55049 tuned whitespace;
wenzelm
parents: 83369
diff changeset
   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
fb39900f0a0f eliminate redundant function;
wenzelm
parents: 83473
diff changeset
   246
        button.textContent = symbol.decoded;
83487
b284ff764c80 clarified tooltip, following Isabelle/jEdit;
wenzelm
parents: 83486
diff changeset
   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
fb39900f0a0f eliminate redundant function;
wenzelm
parents: 83473
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   272
    search_content.id = "search-tab-content";
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   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
53fa51e38c20 clarified names: avoid camel-case;
wenzelm
parents: 83466
diff changeset
   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
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   311
    const state = vscode.getState();
fca677fc8a35 tuned names: avoid camel-case;
wenzelm
parents: 83396
diff changeset
   312
    if (state && state.symbols) {
83469
53fa51e38c20 clarified names: avoid camel-case;
wenzelm
parents: 83466
diff changeset
   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
})();