changeset 63587 | 881e8e2cfec2 |
parent 63579 | 73939a9b70a3 |
child 63761 | 2ca536d0163e |
--- a/src/Pure/General/completion.scala Tue Aug 02 18:58:49 2016 +0200 +++ b/src/Pure/General/completion.scala Tue Aug 02 21:04:52 2016 +0200 @@ -249,7 +249,7 @@ /* word parsers */ - private object Word_Parsers extends RegexParsers + object Word_Parsers extends RegexParsers { override val whiteSpace = "".r