src/Tools/jEdit/src/rendering.scala
changeset 53371 47b23c582127
parent 53272 0dfd78ff7696
child 53571 e58ca0311c0f
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Sep 02 11:03:02 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Sep 02 16:10:26 2013 +0200
     1.3 @@ -77,7 +77,8 @@
     1.4        Keyword.THY_SCRIPT -> LABEL,
     1.5        Keyword.PRF_SCRIPT -> DIGIT,
     1.6        Keyword.PRF_ASM -> KEYWORD3,
     1.7 -      Keyword.PRF_ASM_GOAL -> KEYWORD3
     1.8 +      Keyword.PRF_ASM_GOAL -> KEYWORD3,
     1.9 +      Keyword.PRF_ASM_GOAL_SCRIPT -> DIGIT
    1.10      ).withDefaultValue(KEYWORD1)
    1.11    }
    1.12