changeset 50643 | 09394eaf6804 |
parent 50554 | 0493efcc97e9 |
child 50715 | 8cfd585b9162 |
--- a/src/Tools/jEdit/src/rendering.scala Sun Dec 30 20:15:02 2012 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Sun Dec 30 21:49:20 2012 +0100 @@ -74,7 +74,7 @@ Map[String, Byte]( Keyword.THY_END -> KEYWORD2, Keyword.THY_SCRIPT -> LABEL, - Keyword.PRF_SCRIPT -> LABEL, + Keyword.PRF_SCRIPT -> DIGIT, Keyword.PRF_ASM -> KEYWORD3, Keyword.PRF_ASM_GOAL -> KEYWORD3 ).withDefaultValue(KEYWORD1)