src/Pure/PIDE/rendering.scala
changeset 65145 576d52aa0a78
parent 65144 b5782e996651
child 65149 9dccbebf4511
equal deleted inserted replaced
65144:b5782e996651 65145:576d52aa0a78
    50     val error_message = Value("error_message")
    50     val error_message = Value("error_message")
    51     val message_background_colors =
    51     val message_background_colors =
    52       values -- background_colors -- foreground_colors -- message_underline_colors
    52       values -- background_colors -- foreground_colors -- message_underline_colors
    53 
    53 
    54     // text
    54     // text
    55     val text = Value("text")
    55     val main = Value("main")
    56     val keyword1 = Value("keyword1")
    56     val keyword1 = Value("keyword1")
    57     val keyword2 = Value("keyword2")
    57     val keyword2 = Value("keyword2")
    58     val keyword3 = Value("keyword3")
    58     val keyword3 = Value("keyword3")
    59     val quasi_keyword = Value("quasi_keyword")
    59     val quasi_keyword = Value("quasi_keyword")
    60     val improper = Value("improper")
    60     val improper = Value("improper")
   128     Markup.KEYWORD2 -> Color.keyword2,
   128     Markup.KEYWORD2 -> Color.keyword2,
   129     Markup.KEYWORD3 -> Color.keyword3,
   129     Markup.KEYWORD3 -> Color.keyword3,
   130     Markup.QUASI_KEYWORD -> Color.quasi_keyword,
   130     Markup.QUASI_KEYWORD -> Color.quasi_keyword,
   131     Markup.IMPROPER -> Color.improper,
   131     Markup.IMPROPER -> Color.improper,
   132     Markup.OPERATOR -> Color.operator,
   132     Markup.OPERATOR -> Color.operator,
   133     Markup.STRING -> Color.text,
   133     Markup.STRING -> Color.main,
   134     Markup.ALT_STRING -> Color.text,
   134     Markup.ALT_STRING -> Color.main,
   135     Markup.VERBATIM -> Color.text,
   135     Markup.VERBATIM -> Color.main,
   136     Markup.CARTOUCHE -> Color.text,
   136     Markup.CARTOUCHE -> Color.main,
   137     Markup.LITERAL -> Color.keyword1,
   137     Markup.LITERAL -> Color.keyword1,
   138     Markup.DELIMITER -> Color.text,
   138     Markup.DELIMITER -> Color.main,
   139     Markup.TFREE -> Color.tfree,
   139     Markup.TFREE -> Color.tfree,
   140     Markup.TVAR -> Color.tvar,
   140     Markup.TVAR -> Color.tvar,
   141     Markup.FREE -> Color.free,
   141     Markup.FREE -> Color.free,
   142     Markup.SKOLEM -> Color.skolem,
   142     Markup.SKOLEM -> Color.skolem,
   143     Markup.BOUND -> Color.bound,
   143     Markup.BOUND -> Color.bound,
   149     Markup.CLASS_PARAMETER -> Color.class_parameter,
   149     Markup.CLASS_PARAMETER -> Color.class_parameter,
   150     Markup.ANTIQUOTE -> Color.antiquote,
   150     Markup.ANTIQUOTE -> Color.antiquote,
   151     Markup.ML_KEYWORD1 -> Color.keyword1,
   151     Markup.ML_KEYWORD1 -> Color.keyword1,
   152     Markup.ML_KEYWORD2 -> Color.keyword2,
   152     Markup.ML_KEYWORD2 -> Color.keyword2,
   153     Markup.ML_KEYWORD3 -> Color.keyword3,
   153     Markup.ML_KEYWORD3 -> Color.keyword3,
   154     Markup.ML_DELIMITER -> Color.text,
   154     Markup.ML_DELIMITER -> Color.main,
   155     Markup.ML_NUMERAL -> Color.inner_numeral,
   155     Markup.ML_NUMERAL -> Color.inner_numeral,
   156     Markup.ML_CHAR -> Color.inner_quoted,
   156     Markup.ML_CHAR -> Color.inner_quoted,
   157     Markup.ML_STRING -> Color.inner_quoted,
   157     Markup.ML_STRING -> Color.inner_quoted,
   158     Markup.ML_COMMENT -> Color.inner_comment,
   158     Markup.ML_COMMENT -> Color.inner_comment,
   159     Markup.SML_STRING -> Color.inner_quoted,
   159     Markup.SML_STRING -> Color.inner_quoted,