# HG changeset patch
# User wenzelm
# Date 1646666054 -3600
# Node ID e74d162ddf9f3b44215945049504cbdf5e394f1b
# Parent  90eaac98b3faa0bd4452b427aaa6e8002f2a8a19
clarified char symbols: cover most European languages;

diff -r 90eaac98b3fa -r e74d162ddf9f src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Mar 07 16:01:54 2022 +0100
+++ b/src/Pure/General/symbol.scala	Mon Mar 07 16:14:14 2022 +0100
@@ -36,6 +36,16 @@
   }
 
 
+  /* char symbols */
+
+  private val char_symbols: Array[Symbol] =
+    (0 until 0x500).iterator.map(i => new String(Array(i.toChar))).toArray
+
+  def char_symbol(c: Char): String =
+    if (c < char_symbols.length) char_symbols(c)
+    else c.toString
+
+
   /* ASCII characters */
 
   def is_ascii_printable(c: Char): Boolean = space_char <= c && c <= '~'
@@ -62,7 +72,7 @@
   def ascii(c: Char): Symbol =
   {
     if (c > 127) error("Non-ASCII character: " + quote(c.toString))
-    else char_symbols(c.toInt)
+    else char_symbol(c)
   }
 
   def is_ascii(s: Symbol): Boolean = s.length == 1 && s(0) < 128
@@ -110,21 +120,14 @@
     def match_symbol(i: Int): String =
       match_length(i) match {
         case 0 => ""
-        case 1 =>
-          val c = text.charAt(i)
-          if (c < char_symbols.length) char_symbols(c)
-          else c.toString
-        case n =>
-          text.subSequence(i, i + n).toString
+        case 1 => char_symbol(text.charAt(i))
+        case n => text.subSequence(i, i + n).toString
       }
   }
 
 
   /* iterator */
 
-  private val char_symbols: Array[Symbol] =
-    (0 until 256).iterator.map(i => new String(Array(i.toChar))).toArray
-
   def iterator(text: CharSequence): Iterator[Symbol] =
     new Iterator[Symbol]
     {