# HG changeset patch # User Benedikt Nordhoff # Date 1408735070 -7200 # Fri Aug 22 21:17:50 2014 +0200 # Node ID 849fb4e77aaf51749b0639796467f78984342ee3 # Parent 177eeda93a8cc4c89d59f252e8c10a64b634fbd0 Experimental support for bsup/esup resp. bsub/esub. diff -r 177eeda93a8c -r 849fb4e77aaf src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Fri Aug 22 17:35:48 2014 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Fri Aug 22 21:17:50 2014 +0200 @@ -1,6 +1,6 @@ /* Title: Tools/jEdit/src/token_markup.scala Author: Makarius - + Author: Benedikt Nordhoff Outer syntax token markup. */ @@ -69,7 +69,7 @@ /* extended syntax styles */ - + private val plain_range: Int = JEditToken.ID_COUNT private val full_range = 6 * plain_range + 1 private def check_range(i: Int) { require(0 <= i && i < plain_range) } @@ -140,33 +140,120 @@ def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] = { - // FIXME Symbol.bsub_decoded etc. - 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 + + // Counters for nesting level of bsub/esub resp. bsup/esup + var subcnt = 0 + var supcnt = 0 + + // Active control region: 0 = none, 1 = subscript, 2 = superscript + var active_control = 0 + + // Control style to apply + var control : Option[Byte => Byte] = None + + // Offset to hide before next chare if control becomes active + var hide_if_active = 0 + + // Copy to stable identifiers to allow case distinctions + val SUB_SYM = Symbol.sub_decoded + val SUP_SYM = Symbol.sup_decoded + val BOLD_SYM = Symbol.bold_decoded + val BSUB_SYM = Symbol.bsub_decoded + val BSUP_SYM = Symbol.bsup_decoded + val ESUB_SYM = Symbol.esub_decoded + val ESUP_SYM = Symbol.esup_decoded + + val is_control_to_hide_later = Set (SUB_SYM, SUP_SYM, BOLD_SYM, BSUB_SYM, BSUP_SYM) + val is_control_end = Set (ESUB_SYM, ESUP_SYM) + + def reset_control() { + subcnt = 0 + supcnt = 0 + active_control = 0 + control = None + hide_if_active = 0 + } + + // Check whether a control symbols terminates the active control, used to hide symbol if so + def is_active_end(sym: String) = + subcnt == 0 && active_control == 1 && sym == ESUB_SYM || supcnt == 0 && active_control == 2 && sym == ESUP_SYM + + // Calculates next control state + def update_control(sym: String) { + hide_if_active = 0 + if(active_control == 0) { + sym match { + case SUB_SYM => control = Some(subscript(_)) + case SUP_SYM => control = Some(superscript(_)) + case BOLD_SYM => control = Some(bold(_)) + case BSUB_SYM => control = Some(subscript(_)); active_control = 1 + case BSUP_SYM => control = Some(superscript(_)); active_control = 2 + case _ => control = None + } + if (is_control_to_hide_later(sym)) hide_if_active = sym.length + } + else if (active_control == 1) { + sym match { + case ESUB_SYM if (subcnt == 0) => control = None; active_control = 0 + case _ => control = Some(subscript(_)) + } + } + else if (active_control == 2) { + sym match { + case ESUP_SYM if (supcnt == 0) => control = None; active_control = 0 + case _ => control = Some(superscript(_)) + } + } + } + + // Updates conuters for control nesting + def update_counter(sym: String) { + sym match { + case BSUB_SYM => subcnt += 1 + case BSUP_SYM => supcnt += 1 + case ESUB_SYM => if(subcnt > 0) subcnt -= 1 + case ESUP_SYM => if(supcnt > 0) supcnt -= 1 + case _ => + } + } 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) } + + def apply_control(sym: String, offset: Text.Offset) { + if(is_active_end(sym)) { + // Hide control symbol closing the active control area + mark(offset, offset + sym.length, _ => hidden) + } + else if(control.isDefined && Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) { + // Control is active hide possible leading control symbol + if(hide_if_active > 0) { + mark(offset - hide_if_active, offset, _ => hidden) + } + // Apply control style + mark(offset, offset + sym.length, control.get) + } else { + Symbol.lookup_font(sym) match { + case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _)) + case _ => + } + } + } + + def process_symbol(sym: String, offset:Text.Offset) { + if(sym == "\"") reset_control() + update_counter(sym) + apply_control(sym,offset) + update_control(sym) + } + var offset = 0 - var control = "" + reset_control() for (sym <- Symbol.iterator(text)) { - if (control_style(sym).isDefined) control = sym - else if (control != "") { - if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) { - mark(offset - control.length, offset, _ => hidden) - mark(offset, offset + sym.length, control_style(control).get) - } - control = "" - } - Symbol.lookup_font(sym) match { - case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _)) - case _ => - } + process_symbol(sym, offset) offset += sym.length } result