avoid literal Unicode symbols, which are in danger of being recoded;

--- a/src/Pure/General/mailman.scala	Thu Oct 23 17:14:39 2025 +0200
+++ b/src/Pure/General/mailman.scala	Thu Oct 23 17:52:00 2025 +0200
@@ -200,7 +200,7 @@
       "wmansky:cs/princeton/edu" -> "William Mansky\nwmansky:cs/princeton/edu",
       "y/nemouchi:ensbiotech/edu/dz" -> "Yakoub Nemouchi\ny/nemouchi:ensbiotech/edu/dz",
       "ÐÑÐÐÐÑÐÐÐ ÐÐÐÐÐÐÐÑÐÐÐÑ ÐÐÐÑÐÐÐ" -> "",
-      "∀X/Xπ - Tutorials about Proofs" -> "Bruno Woltzenlogel Paleo",
+      "\u2200X/X\u03c0 - Tutorials about Proofs" -> "Bruno Woltzenlogel Paleo",
     )
 
   private def tune(s: String): String =

--- a/src/Tools/VSCode/extension/media/sledgehammer.js	Thu Oct 23 17:14:39 2025 +0200
+++ b/src/Tools/VSCode/extension/media/sledgehammer.js	Thu Oct 23 17:52:00 2025 +0200
@@ -31,7 +31,7 @@
   chevronBtn.className = 'provers-dropdown-toggle';
   chevronBtn.setAttribute('aria-label', 'Show provers history');
   chevronBtn.tabIndex = -1;
-  chevronBtn.innerHTML = '▼';
+  chevronBtn.innerHTML = '\u25bc';
   proversInputWrapper.appendChild(chevronBtn);
 
   proversLabel.appendChild(proversInputWrapper);
@@ -63,7 +63,7 @@
         row.textContent = item;
 
         const delBtn = document.createElement('span');
-        delBtn.textContent = '✖';
+        delBtn.textContent = '\u2716';
         delBtn.className = 'delete-btn';
         delBtn.title = 'Delete entry';
         delBtn.addEventListener('mousedown', function (ev) {

--- a/src/Tools/VSCode/extension/media/symbols.js	Thu Oct 23 17:14:39 2025 +0200
+++ b/src/Tools/VSCode/extension/media/symbols.js	Thu Oct 23 17:52:00 2025 +0200
@@ -109,10 +109,10 @@
     let i = 0;
     while (i < symbol.length) {
       const char = symbol[i];
-      if (char === "⇧") {
+      if (char === "\u21e7") {
         i++;
         if (i < symbol.length) result += "<sup>" + symbol[i] + "</sup>";
-      } else if (char === "⇩") { 
+      } else if (char === "\u21e9") { 
         i++;
         if (i < symbol.length) result += "<sub>" + symbol[i] + "</sub>";
       } else {
@@ -128,13 +128,13 @@
   let i = 0;
   while (i < symbol.length) {
     const char = symbol[i];
-    if (char === "⇧") {
+    if (char === "\u21e7") {
       i++;
       if (i < symbol.length) {
         if (controlSup) result += controlSup + symbol[i];
         else result += symbol[i];
       }
-    } else if (char === "⇩") {
+    } else if (char === "\u21e9") {
       i++;
       if (i < symbol.length) {
         if (controlSub) result += controlSub + symbol[i];

--- a/src/Tools/VSCode/extension/src/script_decorations.ts	Thu Oct 23 17:14:39 2025 +0200
+++ b/src/Tools/VSCode/extension/src/script_decorations.ts	Thu Oct 23 17:52:00 2025 +0200
@@ -9,12 +9,12 @@
   TextDocument, TextEditor, window, workspace } from 'vscode'
 
 const arrows = {
-  sub: '⇩',
-  sup: '⇧',
-  sub_begin: '⇘',
-  sub_end: '⇙',
-  sup_begin: '⇗',
-  sup_end: '⇖'
+  sub: '\u21e9',
+  sup: '\u21e7',
+  sub_begin: '\u21d8',
+  sub_end: '\u21d9',
+  sup_begin: '\u21d7',
+  sup_end: '\u21d6'
 }
 const no_hide_list = [' ', '\n', '\r', ...Object.values(arrows)]