src/Tools/jEdit/src/jedit_rendering.scala
changeset 67438 fdb7b995974d
parent 67365 fb539f83683a
child 67439 78759a7bd874
equal deleted inserted replaced
67437:a6bf7167c5e1 67438:fdb7b995974d
    86       ML_Lex.Kind.INT -> DIGIT,
    86       ML_Lex.Kind.INT -> DIGIT,
    87       ML_Lex.Kind.REAL -> DIGIT,
    87       ML_Lex.Kind.REAL -> DIGIT,
    88       ML_Lex.Kind.CHAR -> LITERAL2,
    88       ML_Lex.Kind.CHAR -> LITERAL2,
    89       ML_Lex.Kind.STRING -> LITERAL1,
    89       ML_Lex.Kind.STRING -> LITERAL1,
    90       ML_Lex.Kind.SPACE -> NULL,
    90       ML_Lex.Kind.SPACE -> NULL,
    91       ML_Lex.Kind.COMMENT -> COMMENT1,
    91       ML_Lex.Kind.INFORMAL_COMMENT -> COMMENT1,
    92       ML_Lex.Kind.COMMENT_CARTOUCHE -> COMMENT1,
    92       ML_Lex.Kind.FORMAL_COMMENT -> COMMENT1,
    93       ML_Lex.Kind.ANTIQ -> NULL,
    93       ML_Lex.Kind.ANTIQ -> NULL,
    94       ML_Lex.Kind.ANTIQ_START -> LITERAL4,
    94       ML_Lex.Kind.ANTIQ_START -> LITERAL4,
    95       ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,
    95       ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,
    96       ML_Lex.Kind.ANTIQ_OTHER -> NULL,
    96       ML_Lex.Kind.ANTIQ_OTHER -> NULL,
    97       ML_Lex.Kind.ANTIQ_STRING -> NULL,
    97       ML_Lex.Kind.ANTIQ_STRING -> NULL,