font style for literal control symbols, notably for antiquotations;
authorwenzelm
Mon Dec 04 17:37:26 2017 +0100 (7 months ago)
changeset 67127cf111622c9f8
parent 67126 143f0ba01415
child 67128 4d91b6d5d49c
font style for literal control symbols, notably for antiquotations;
src/Pure/General/symbol.scala
src/Tools/jEdit/src/syntax_style.scala
     1.1 --- a/src/Pure/General/symbol.scala	Mon Dec 04 16:28:06 2017 +0100
     1.2 +++ b/src/Pure/General/symbol.scala	Mon Dec 04 17:37:26 2017 +0100
     1.3 @@ -577,8 +577,14 @@
     1.4  
     1.5    /* control symbols */
     1.6  
     1.7 +  val control_prefix = "\\<^"
     1.8 +  val control_suffix = ">"
     1.9 +
    1.10 +  def is_control_encoded(sym: Symbol): Boolean =
    1.11 +    sym.startsWith(control_prefix) && sym.endsWith(control_suffix)
    1.12 +
    1.13    def is_control(sym: Symbol): Boolean =
    1.14 -    (sym.startsWith("\\<^") && sym.endsWith(">")) || symbols.control_decoded.contains(sym)
    1.15 +    is_control_encoded(sym) || symbols.control_decoded.contains(sym)
    1.16  
    1.17    def is_controllable(sym: Symbol): Boolean =
    1.18      !is_blank(sym) && !is_control(sym) && !is_open(sym) && !is_close(sym) &&
     2.1 --- a/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 16:28:06 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 17:37:26 2017 +0100
     2.3 @@ -90,36 +90,50 @@
     2.4      }
     2.5    }
     2.6  
     2.7 +  private def control_style(sym: String): Option[Byte => Byte] =
     2.8 +    if (sym == Symbol.sub_decoded) Some(subscript(_))
     2.9 +    else if (sym == Symbol.sup_decoded) Some(superscript(_))
    2.10 +    else if (sym == Symbol.bold_decoded) Some(bold(_))
    2.11 +    else None
    2.12 +
    2.13    def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] =
    2.14    {
    2.15 -    def control_style(sym: String): Option[Byte => Byte] =
    2.16 -      if (sym == Symbol.sub_decoded) Some(subscript(_))
    2.17 -      else if (sym == Symbol.sup_decoded) Some(superscript(_))
    2.18 -      else if (sym == Symbol.bold_decoded) Some(bold(_))
    2.19 -      else None
    2.20 -
    2.21      var result = Map[Text.Offset, Byte => Byte]()
    2.22      def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
    2.23      {
    2.24        for (i <- start until stop) result += (i -> style)
    2.25      }
    2.26 +
    2.27      var offset = 0
    2.28      var control = ""
    2.29      for (sym <- Symbol.iterator(text)) {
    2.30 +      val end_offset = offset + sym.length
    2.31 +
    2.32        if (control_style(sym).isDefined) control = sym
    2.33        else if (control != "") {
    2.34          if (Symbol.is_controllable(sym) && !Symbol.fonts.isDefinedAt(sym)) {
    2.35            mark(offset - control.length, offset, _ => hidden)
    2.36 -          mark(offset, offset + sym.length, control_style(control).get)
    2.37 +          mark(offset, end_offset, control_style(control).get)
    2.38          }
    2.39          control = ""
    2.40        }
    2.41 +
    2.42 +      if (Symbol.is_control_encoded(sym)) {
    2.43 +        val a = offset + Symbol.control_prefix.length
    2.44 +        val b = end_offset - Symbol.control_suffix.length
    2.45 +        mark(offset, a, _ => hidden)
    2.46 +        mark(a, b, _ => JEditToken.KEYWORD4)
    2.47 +        mark(b, end_offset, _ => hidden)
    2.48 +      }
    2.49 +
    2.50        Symbol.lookup_font(sym) match {
    2.51 -        case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
    2.52 +        case Some(idx) => mark(offset, end_offset, user_font(idx, _))
    2.53          case _ =>
    2.54        }
    2.55 -      offset += sym.length
    2.56 +
    2.57 +      offset = end_offset
    2.58      }
    2.59 +
    2.60      result
    2.61    }
    2.62