equal
deleted
inserted
replaced
38 |
38 |
39 val empty: Lexicon = new Lexicon(empty_tree) |
39 val empty: Lexicon = new Lexicon(empty_tree) |
40 def apply(elems: String*): Lexicon = empty ++ elems |
40 def apply(elems: String*): Lexicon = empty ++ elems |
41 } |
41 } |
42 |
42 |
43 class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers |
43 final class Lexicon private(main_tree: Lexicon.Tree) extends RegexParsers |
44 { |
44 { |
45 import Lexicon.Tree |
45 import Lexicon.Tree |
46 |
46 |
47 |
47 |
48 /* auxiliary operations */ |
48 /* auxiliary operations */ |