changeset 46712 | 8650d9a95736 |
parent 46627 | fbe2cb05bdb3 |
child 48342 | 4a8f06cbf8bb |
--- a/src/Pure/General/scan.scala Mon Feb 27 16:56:25 2012 +0100 +++ b/src/Pure/General/scan.scala Mon Feb 27 17:13:25 2012 +0100 @@ -40,7 +40,7 @@ def apply(elems: String*): Lexicon = empty ++ elems } - class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers + final class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers { import Lexicon.Tree