font style for literal control symbols, notably for antiquotations;

--- a/src/Pure/General/symbol.scala	Mon Dec 04 16:28:06 2017 +0100
+++ b/src/Pure/General/symbol.scala	Mon Dec 04 17:37:26 2017 +0100
@@ -577,8 +577,14 @@
 
   /* control symbols */
 
+  val control_prefix = "\\<^"
+  val control_suffix = ">"
+
+  def is_control_encoded(sym: Symbol): Boolean =
+    sym.startsWith(control_prefix) && sym.endsWith(control_suffix)
+
   def is_control(sym: Symbol): Boolean =
-    (sym.startsWith("\\<^") && sym.endsWith(">")) || symbols.control_decoded.contains(sym)
+    is_control_encoded(sym) || symbols.control_decoded.contains(sym)
 
   def is_controllable(sym: Symbol): Boolean =
     !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) &&

--- a/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 16:28:06 2017 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 17:37:26 2017 +0100
@@ -90,36 +90,50 @@
     }
   }
 
+  private def control_style(sym: String): Option[Byte => Byte] =
+    if (sym == Symbol.sub_decoded) Some(subscript(_))
+    else if (sym == Symbol.sup_decoded) Some(superscript(_))
+    else if (sym == Symbol.bold_decoded) Some(bold(_))
+    else None
+
   def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] =
   {
-    def control_style(sym: String): Option[Byte => Byte] =
-      if (sym == Symbol.sub_decoded) Some(subscript(_))
-      else if (sym == Symbol.sup_decoded) Some(superscript(_))
-      else if (sym == Symbol.bold_decoded) Some(bold(_))
-      else None
-
     var result = Map[Text.Offset, Byte => Byte]()
     def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
     {
       for (i <- start until stop) result += (i -> style)
     }
+
     var offset = 0
     var control = ""
     for (sym <- Symbol.iterator(text)) {
+      val end_offset = offset + sym.length
+
       if (control_style(sym).isDefined) control = sym
       else if (control != "") {
         if (Symbol.is_controllable(sym) && !Symbol.fonts.isDefinedAt(sym)) {
           mark(offset - control.length, offset, _ => hidden)
-          mark(offset, offset + sym.length, control_style(control).get)
+          mark(offset, end_offset, control_style(control).get)
         }
         control = ""
       }
+
+      if (Symbol.is_control_encoded(sym)) {
+        val a = offset + Symbol.control_prefix.length
+        val b = end_offset - Symbol.control_suffix.length
+        mark(offset, a, _ => hidden)
+        mark(a, b, _ => JEditToken.KEYWORD4)
+        mark(b, end_offset, _ => hidden)
+      }
+
       Symbol.lookup_font(sym) match {
-        case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
+        case Some(idx) => mark(offset, end_offset, user_font(idx, _))
         case _ =>
       }
-      offset += sym.length
+
+      offset = end_offset
     }
+
     result
   }