src/Tools/VSCode/extension/src/script_decorations.ts

--- 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)]