clarified rendering: use COMMENT4 elsewhere;
authorwenzelm
Sun Mar 24 17:19:30 2019 +0100 (2 months ago)
changeset 69963396e0120f7b8
parent 69962 82e945d472d5
child 69964 699ffc7cbab8
clarified rendering: use COMMENT4 elsewhere;
src/Tools/jEdit/src/jedit_rendering.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Sun Mar 24 13:48:46 2019 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Sun Mar 24 17:19:30 2019 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4        Token.Kind.STRING -> LITERAL1,
     1.5        Token.Kind.ALT_STRING -> LITERAL2,
     1.6        Token.Kind.VERBATIM -> COMMENT3,
     1.7 -      Token.Kind.CARTOUCHE -> COMMENT4,
     1.8 +      Token.Kind.CARTOUCHE -> COMMENT3,
     1.9        Token.Kind.INFORMAL_COMMENT -> COMMENT1,
    1.10        Token.Kind.FORMAL_COMMENT -> COMMENT1,
    1.11        Token.Kind.ERROR -> INVALID