clarified rendering, notably of \<^latex>CARTOUCHE in outer syntax;
authorwenzelm
Sun Mar 24 18:38:42 2019 +0100 (4 weeks ago)
changeset 69970b5a47478897a
parent 69969 c211db89f916
child 69971 4e98239aa083
clarified rendering, notably of \<^latex>CARTOUCHE in outer syntax;
src/Pure/PIDE/rendering.scala
     1.1 --- a/src/Pure/PIDE/rendering.scala	Sun Mar 24 18:30:59 2019 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Sun Mar 24 18:38:42 2019 +0100
     1.3 @@ -139,6 +139,7 @@
     1.4      Markup.ML_CHAR -> Color.inner_quoted,
     1.5      Markup.ML_STRING -> Color.inner_quoted,
     1.6      Markup.ML_COMMENT -> Color.comment1,
     1.7 +    Markup.COMMENT -> Color.comment1,
     1.8      Markup.COMMENT1 -> Color.comment1,
     1.9      Markup.COMMENT2 -> Color.comment2,
    1.10      Markup.COMMENT3 -> Color.comment3)