--- a/src/Tools/jEdit/src/token_markup.scala Mon Jun 20 12:13:43 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Mon Jun 20 22:43:56 2011 +0200
@@ -9,9 +9,13 @@
import isabelle._
+import java.awt.{Font, Color}
+import java.awt.font.TextAttribute
+
+import org.gjt.sp.util.SyntaxUtilities
import org.gjt.sp.jedit.Mode
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler,
- ParserRuleSet, ModeProvider, XModeHandler}
+ ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
import javax.swing.text.Segment
@@ -21,6 +25,7 @@
/* extended syntax styles */
private val plain_range: Int = JEditToken.ID_COUNT
+ private val full_range: Int = 4 * plain_range + 1
private def check_range(i: Int) { require(0 <= i && i < plain_range) }
def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
@@ -28,38 +33,64 @@
def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
val hidden: Byte = (4 * plain_range).toByte
+ private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
+ {
+ import scala.collection.JavaConversions._
+ val font = style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
+ new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, font)
+ }
+
+ private def bold_style(style: SyntaxStyle): SyntaxStyle =
+ new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor,
+ style.getFont.deriveFont(Font.BOLD))
+
+ class Style_Extender extends SyntaxUtilities.StyleExtender
+ {
+ override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
+ {
+ val new_styles = new Array[SyntaxStyle](full_range)
+ for (i <- 0 until plain_range) {
+ val style = styles(i)
+ new_styles(i) = style
+ 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)
+ }
+ new_styles(hidden) =
+ new SyntaxStyle(Color.white, null, new Font(styles(0).getFont.getFamily, 0, 1))
+ new_styles
+ }
+ }
+
private def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
: Map[Text.Offset, Byte => Byte] =
{
- if (Isabelle.extended_styles) {
- // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
- def ctrl_style(sym: String): Option[Byte => Byte] =
- if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
- else if (symbols.is_superscript_decoded(sym)) Some(superscript(_))
- else if (symbols.is_bold_decoded(sym)) Some(bold(_))
- else None
+ // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
+ def ctrl_style(sym: String): Option[Byte => Byte] =
+ if (symbols.is_subscript_decoded(sym)) Some(subscript(_))
+ else if (symbols.is_superscript_decoded(sym)) Some(superscript(_))
+ else if (symbols.is_bold_decoded(sym)) 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 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 ctrl = ""
+ for (sym <- Symbol.iterator(text).map(_.toString)) {
+ if (ctrl_style(sym).isDefined) ctrl = sym
+ else if (ctrl != "") {
+ if (symbols.is_controllable(sym) && sym != "\"") {
+ mark(offset - ctrl.length, offset, _ => hidden)
+ mark(offset, offset + sym.length, ctrl_style(ctrl).get)
+ }
+ ctrl = ""
}
- var offset = 0
- var ctrl = ""
- for (sym <- Symbol.iterator(text).map(_.toString)) {
- if (ctrl_style(sym).isDefined) ctrl = sym
- else if (ctrl != "") {
- if (symbols.is_controllable(sym) && sym != "\"") {
- mark(offset - ctrl.length, offset, _ => hidden)
- mark(offset, offset + sym.length, ctrl_style(ctrl).get)
- }
- ctrl = ""
- }
- offset += sym.length
- }
- result
+ offset += sym.length
}
- else Map.empty
+ result
}