changeset 66984 | a1d3e5df0c95 |
parent 66768 | f27488f47a47 |
child 66985 | 7382ff5b46b9 |
--- a/src/Pure/General/completion.scala Wed Nov 01 20:46:23 2017 +0100 +++ b/src/Pure/General/completion.scala Wed Nov 01 21:02:16 2017 +0100 @@ -256,7 +256,8 @@ /* init */ val empty: Completion = new Completion() - def init(): Completion = + + lazy val init: Completion = empty.add_symbols.add_abbrevs(Completion.symbol_abbrevs ::: Completion.default_abbrevs)