author | wenzelm |
Sun, 30 Dec 2012 21:49:20 +0100 | |
changeset 50643 | 09394eaf6804 |
parent 50642 | aca12f646772 |
child 50644 | d15f1c39401c |
--- 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)