>From c12a888e3269247ba4ff583cd31d68967f7ad7ec Mon Sep 17 00:00:00 2001
From: Rafal Kolanski <rafal.kolanski@nicta.com.au>
Date: Wed, 2 Sep 2015 10:27:12 +1000
Subject: [PATCH] Redo Isabelle plugin chunk rendering.

(depends on jedit patch
 0003-Allow-specification-of-sizes-for-fallback-fonts.patch,
 see: https://sourceforge.net/p/jedit/patches/569/ )

Use AttributeString and jEdit's information on font substitution.
Simplify code greatly, use existing jEdit options to set up the fonts,
get rid of max_user_fonts = 2 restriction, and free up 19*2 slots in the
extended styles table (which can then be used for a second layer of
sub&superscript).

Font specification in etc/symbols is now ignored.

Tested with missing glyphs, user font fallbacks, symbol font fallbacks
and code points above 0xFFFF (take up two or more chars in Java).
Checked that overlap with jEdit internal chunk glyphs is pixel-perfect.
---
 src/Tools/jEdit/src/rich_text_area.scala | 108 ++++++++++++++++++-------------
 src/Tools/jEdit/src/token_markup.scala   |  19 +-----
 2 files changed, 67 insertions(+), 60 deletions(-)

diff --git a/src/Tools/jEdit/src/rich_text_area.scala b/src/Tools/jEdit/src/rich_text_area.scala
index 66a23a7..2afb5d7 100644
--- a/src/Tools/jEdit/src/rich_text_area.scala
+++ b/src/Tools/jEdit/src/rich_text_area.scala
@@ -10,7 +10,7 @@ package isabelle.jedit
 
 import isabelle._
 
-import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor, MouseInfo}
+import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor, MouseInfo, Font}
 import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
   FocusAdapter, FocusEvent, WindowEvent, WindowAdapter, InputEvent}
 import java.awt.font.TextAttribute
@@ -357,6 +357,50 @@ class Rich_Text_Area(
     else rendering.caret_invisible_color
   }
 
+  private class CustomChunk(line_start: Text.Offset, chunk: Chunk)
+  {
+    val offset : Text.Offset = line_start + chunk.offset
+    val str : String = if (chunk.str == null) " " * chunk.length else chunk.str
+    val astr : AttributedString = new AttributedString(str)
+
+    astr.addAttribute(TextAttribute.FONT, chunk.style.getFont)
+    astr.addAttribute(TextAttribute.FOREGROUND, chunk.style.getForegroundColor)
+
+    def addAttributeRange(range: Text.Range, attr: TextAttribute, o: Object) =
+      astr.addAttribute(attr, o, range.start - offset, range.stop - offset)
+
+    def addTextColorRange(range: Text.Range, color: Color) =
+      addAttributeRange(range, TextAttribute.FOREGROUND, color)
+
+    def draw(gfx: Graphics2D, x: Float , y: Float) =
+      gfx.drawString(astr.getIterator, x, y)
+
+    def deriveSubstFont(codepoint: Int): Font =
+    {
+      val mainFont = chunk.style.getFont()
+      Chunk.getSubstFont(codepoint) match {
+        case substFont: Font => Chunk.deriveSubstFont(mainFont, substFont)
+        case _ => mainFont
+      }
+    }
+
+    def doSubstFonts()
+    {
+      if (chunk.usedFontSubstitution()) {
+        val mainFont = chunk.style.getFont
+        var i = mainFont.canDisplayUpTo(astr.getIterator(), 0, str.length)
+
+        while (i >= 0 && i < str.length)
+        {
+          val next = str.offsetByCodePoints(i, 1)
+          val substFont = deriveSubstFont(str.codePointAt(i))
+          astr.addAttribute(TextAttribute.FONT, substFont, i, next)
+          i = mainFont.canDisplayUpTo(astr.getIterator(), next, str.length)
+        }
+      }
+    }
+  }
+
   private def paint_chunk_list(rendering: Rendering,
     gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   {
@@ -370,66 +414,42 @@ class Rich_Text_Area(
 
     var w = 0.0f
     var chunk = head
+
     while (chunk != null) {
-      val chunk_offset = line_start + chunk.offset
+
       if (x + w + chunk.width > clip_rect.x &&
           x + w < clip_rect.x + clip_rect.width && chunk.length > 0)
       {
-        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
-        val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
-        val chunk_font = chunk.style.getFont
-        val chunk_color = chunk.style.getForegroundColor
+        val cc = new CustomChunk(line_start, chunk)
 
-        def string_width(s: String): Float =
-          if (s.isEmpty) 0.0f
-          else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
+        val chunk_offset = line_start + chunk.offset
+        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
 
         val markup =
           for {
-            r1 <- rendering.text_color(chunk_range, chunk_color)
+            r1 <- rendering.text_color(chunk_range, chunk.style.getForegroundColor)
             r2 <- r1.try_restrict(chunk_range)
           } yield r2
 
-        val padded_markup_iterator =
-          if (markup.isEmpty)
-            Iterator(Text.Info(chunk_range, chunk_color))
-          else
-            Iterator(
-              Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
-            markup.iterator ++
-            Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
-
-        var x1 = x + w
-        gfx.setFont(chunk_font)
-        for (Text.Info(range, color) <- padded_markup_iterator if !range.is_singularity) {
-          val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
-          gfx.setColor(color)
+        // mark Isabelle colors
+        for (Text.Info(range, color) <- markup.iterator if !range.is_singularity)
+        {
+          cc.addTextColorRange(range, color)
 
+          // flip colors in cursor
           range.try_restrict(caret_range) match {
-            case Some(r) if !r.is_singularity =>
-              val i = r.start - range.start
-              val j = r.stop - range.start
-              val s1 = str.substring(0, i)
-              val s2 = str.substring(i, j)
-              val s3 = str.substring(j)
-
-              if (s1.nonEmpty) gfx.drawString(s1, x1, y)
-
-              val astr = new AttributedString(s2)
-              astr.addAttribute(TextAttribute.FONT, chunk_font)
-              astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering))
-              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
-              gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
-
-              if (s3.nonEmpty)
-                gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
-
+            case Some(r) if !r.is_singularity => {
+              cc.addAttributeRange(r, TextAttribute.FOREGROUND, caret_color(rendering))
+              cc.addAttributeRange(r, TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
+            }
             case _ =>
-              gfx.drawString(str, x1, y)
           }
-          x1 += string_width(str)
         }
+
+        cc.doSubstFonts()
+        cc.draw(gfx, x + w, y)
       }
+
       w += chunk.width
       chunk = chunk.next.asInstanceOf[Chunk]
     }
diff --git a/src/Tools/jEdit/src/token_markup.scala b/src/Tools/jEdit/src/token_markup.scala
index 9c6edcd..9c941fd 100644
--- a/src/Tools/jEdit/src/token_markup.scala
+++ b/src/Tools/jEdit/src/token_markup.scala
@@ -74,7 +74,6 @@ object Token_Markup
   def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
   def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
   def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
-  def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte }
   val hidden: Byte = (6 * plain_range).toByte
 
   private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle =
@@ -107,11 +106,6 @@ object Token_Markup
 
   class Style_Extender extends SyntaxUtilities.StyleExtender
   {
-    val max_user_fonts = 2
-    if (Symbol.font_names.length > max_user_fonts)
-      error("Too many user symbol fonts (" + max_user_fonts + " permitted): " +
-        Symbol.font_names.mkString(", "))
-
     override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
     {
       val new_styles = new Array[SyntaxStyle](full_range)
@@ -127,16 +121,13 @@ object Token_Markup
         new_styles(subscript(i.toByte)) = script_style(style, -1)
         new_styles(superscript(i.toByte)) = script_style(style, 1)
         new_styles(bold(i.toByte)) = bold_style(style)
-        for (idx <- 0 until max_user_fonts)
-          new_styles(user_font(idx, i.toByte)) = style
-        for ((family, idx) <- Symbol.font_index)
-          new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(_, family))
       }
+
       new_styles(hidden) =
         new SyntaxStyle(hidden_color, null,
           { val font = styles(0).getFont
-            GUI.transform_font(new Font(font.getFamily, 0, 1),
-              AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
+            GUI.transform_font(new Font(font.getFamily, 0, font.getSize),
+              AffineTransform.getScaleInstance(1.0/font.getSize.toDouble, 1.0)) })
       new_styles
     }
   }
@@ -166,10 +157,6 @@ object Token_Markup
         }
         control = ""
       }
-      Symbol.lookup_font(sym) match {
-        case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
-        case _ =>
-      }
       offset += sym.length
     }
     result
-- 
2.1.0

