1.1 --- a/src/Pure/General/markup.scala	Tue Jun 14 13:34:27 2011 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Tue Jun 14 14:33:46 2011 +0200
     1.3 @@ -167,6 +167,7 @@
     1.4    val XNUM = "xnum"
     1.5    val XSTR = "xstr"
     1.6    val LITERAL = "literal"
     1.7 +  val INNER_STRING = "inner_string"
     1.8    val INNER_COMMENT = "inner_comment"
     1.9  
    1.10    val TOKEN_RANGE = "token_range"

     2.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Tue Jun 14 13:34:27 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Tue Jun 14 14:33:46 2011 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4  
     2.5  import java.awt.Color
     2.6  
     2.7 +import org.lobobrowser.util.gui.ColorFactory
     2.8  import org.gjt.sp.jedit.syntax.Token
     2.9  
    2.10  
    2.11 @@ -20,6 +21,8 @@
    2.12  
    2.13    // see http://www.w3schools.com/css/css_colornames.asp
    2.14  
    2.15 +  def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
    2.16 +
    2.17    val outdated_color = new Color(240, 240, 240)
    2.18    val unfinished_color = new Color(255, 228, 225)
    2.19  
    2.20 @@ -30,10 +33,6 @@
    2.21    val bad_color = new Color(255, 106, 106, 100)
    2.22    val hilite_color = new Color(255, 204, 102, 100)
    2.23  
    2.24 -  val free_color = new Color(0, 0, 0xFF)
    2.25 -  val skolem_color = new Color(0xD2, 0x69, 0x1E)
    2.26 -  val bound_color = new Color(0, 0x80, 0)
    2.27 -
    2.28    class Icon(val priority: Int, val icon: javax.swing.Icon)
    2.29    {
    2.30      def >= (that: Icon): Boolean = this.priority >= that.priority
    2.31 @@ -106,11 +105,33 @@
    2.32      case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
    2.33    }
    2.34  
    2.35 +  private val foreground_colors: Map[String, Color] =
    2.36 +    Map(
    2.37 +      Markup.TCLASS -> get_color("red"),
    2.38 +      Markup.TFREE -> get_color("#A020F0"),
    2.39 +      Markup.TVAR -> get_color("#A020F0"),
    2.40 +      Markup.CONST -> get_color("dimgrey"),
    2.41 +      Markup.FREE -> get_color("blue"),
    2.42 +      Markup.SKOLEM -> get_color("#D2691E"),
    2.43 +      Markup.BOUND -> get_color("green"),
    2.44 +      Markup.VAR -> get_color("#00009B"),
    2.45 +      Markup.INNER_STRING -> get_color("#D2691E"),
    2.46 +      Markup.INNER_COMMENT -> get_color("#8B0000"),
    2.47 +      Markup.DYNAMIC_FACT -> get_color("yellowgreen"),
    2.48 +      Markup.LITERAL -> get_color("black"),
    2.49 +      Markup.ML_KEYWORD -> get_color("grey"),
    2.50 +      Markup.ML_DELIMITER -> get_color("black"),
    2.51 +      Markup.ML_NUMERAL -> get_color("red"),
    2.52 +      Markup.ML_CHAR -> get_color("#D2691E"),
    2.53 +      Markup.ML_STRING -> get_color("#D2691E"),
    2.54 +      Markup.ML_COMMENT -> get_color("#8B0000"),
    2.55 +      Markup.ML_MALFORMED -> get_color("#FF6A6A")
    2.56 +    )
    2.57 +
    2.58    val foreground: Markup_Tree.Select[Color] =
    2.59    {
    2.60 -    case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => free_color
    2.61 -    case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => skolem_color
    2.62 -    case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => bound_color
    2.63 +    case Text.Info(_, XML.Elem(Markup(m, _), _))
    2.64 +    if foreground_colors.isDefinedAt(m) => foreground_colors(m)
    2.65    }
    2.66  
    2.67    val tooltip: Markup_Tree.Select[String] =
    2.68 @@ -162,39 +183,6 @@
    2.69    {
    2.70      import Token._
    2.71      Map[String, Byte](
    2.72 -      // logical entities
    2.73 -      Markup.TCLASS -> NULL,
    2.74 -      Markup.TYCON -> NULL,
    2.75 -      Markup.FIXED -> NULL,
    2.76 -      Markup.CONST -> LITERAL2,
    2.77 -      Markup.DYNAMIC_FACT -> LABEL,
    2.78 -      // inner syntax
    2.79 -      Markup.TFREE -> NULL,
    2.80 -      Markup.FREE -> NULL,
    2.81 -      Markup.TVAR -> NULL,
    2.82 -      Markup.SKOLEM -> NULL,
    2.83 -      Markup.BOUND -> NULL,
    2.84 -      Markup.VAR -> NULL,
    2.85 -      Markup.NUM -> DIGIT,
    2.86 -      Markup.FLOAT -> DIGIT,
    2.87 -      Markup.XNUM -> DIGIT,
    2.88 -      Markup.XSTR -> LITERAL4,
    2.89 -      Markup.LITERAL -> OPERATOR,
    2.90 -      Markup.INNER_COMMENT -> COMMENT1,
    2.91 -      Markup.SORT -> NULL,
    2.92 -      Markup.TYP -> NULL,
    2.93 -      Markup.TERM -> NULL,
    2.94 -      Markup.PROP -> NULL,
    2.95 -      // ML syntax
    2.96 -      Markup.ML_KEYWORD -> KEYWORD1,
    2.97 -      Markup.ML_DELIMITER -> OPERATOR,
    2.98 -      Markup.ML_IDENT -> NULL,
    2.99 -      Markup.ML_TVAR -> NULL,
   2.100 -      Markup.ML_NUMERAL -> DIGIT,
   2.101 -      Markup.ML_CHAR -> LITERAL1,
   2.102 -      Markup.ML_STRING -> LITERAL1,
   2.103 -      Markup.ML_COMMENT -> COMMENT1,
   2.104 -      Markup.ML_MALFORMED -> INVALID,
   2.105        // embedded source text
   2.106        Markup.ML_SOURCE -> COMMENT3,
   2.107        Markup.DOC_SOURCE -> COMMENT3,