# HG changeset patch
# User wenzelm
# Date 1591877584 -7200
# Node ID aec0f7b58cc60b05ec5885c009b653badfdab77d
# Parent  65fd0f032a75c19d9da0389ec165315cb32614b6
proper rendering of complex codepoints, e.g. \<^url> code: 0x01F310;

diff -r 65fd0f032a75 -r aec0f7b58cc6 src/Pure/General/codepoint.scala
--- a/src/Pure/General/codepoint.scala	Wed Jun 10 19:59:12 2020 +0200
+++ b/src/Pure/General/codepoint.scala	Thu Jun 11 14:13:04 2020 +0200
@@ -6,22 +6,29 @@
 
 package isabelle
 
+import isabelle.Text.Offset
+
 
 object Codepoint
 {
   def string(c: Int): String = new String(Array(c), 0, 1)
 
-  def iterator(s: String): Iterator[Int] =
-    new Iterator[Int] {
-      var offset = 0
-      def hasNext: Boolean = offset < s.length
-      def next: Int =
-      {
-        val c = s.codePointAt(offset)
-        offset += Character.charCount(c)
-        c
-      }
+  private class Iterator_Offset[A](s: String, result: (Int, Text.Offset) => A)
+    extends Iterator[A]
+  {
+    var offset = 0
+    def hasNext: Boolean = offset < s.length
+    def next: A =
+    {
+      val c = s.codePointAt(offset)
+      val i = offset
+      offset += Character.charCount(c)
+      result(c, i)
     }
+  }
+
+  def iterator_offset(s: String): Iterator[(Int, Text.Offset)] = new Iterator_Offset(s, (_, _))
+  def iterator(s: String): Iterator[Int] = new Iterator_Offset(s, (c, _) => c)
 
   def length(s: String): Int = iterator(s).length
 }
diff -r 65fd0f032a75 -r aec0f7b58cc6 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Wed Jun 10 19:59:12 2020 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Thu Jun 11 14:13:04 2020 +0200
@@ -267,19 +267,19 @@
           }
 
         val extended = Syntax_Style.extended(line)
+        def special(i: Int): Boolean = extended.isDefinedAt(i) || line.charAt(i) == '\t'
 
         var offset = 0
         for ((style, token) <- styled_tokens) {
           val length = token.length
-          val offsets = offset until (offset + length)
-          if (offsets.exists(i => extended.isDefinedAt(i) || line.charAt(i) == '\t')) {
-            for (i <- offsets) {
+          if ((offset until (offset + length)).exists(special)) {
+            for ((c, i) <- Codepoint.iterator_offset(token)) {
               val style1 =
-                extended.get(i) match {
+                extended.get(offset + i) match {
                   case None => style
                   case Some(ext) => ext(style)
                 }
-              handler.handleToken(line, style1, i, 1, context1)
+              handler.handleToken(line, style1, offset + i, Character.charCount(c), context1)
             }
           }
           else handler.handleToken(line, style, offset, length, context1)