src/Pure/Thy/completion.scala

--- a/src/Pure/Thy/completion.scala	Thu Feb 23 19:58:49 2012 +0100
+++ b/src/Pure/Thy/completion.scala	Thu Feb 23 20:23:19 2012 +0100
@@ -12,9 +12,7 @@
 
 object Completion
 {
-  val empty: Completion =
-    new Completion(Scan.Lexicon(), Map.empty, Scan.Lexicon(), Map.empty)
-
+  val empty: Completion = new Completion()
   def init(): Completion = empty.add_symbols()
 
 
@@ -43,10 +41,10 @@
 }
 
 class Completion private(
-  words_lex: Scan.Lexicon,
-  words_map: Map[String, String],
-  abbrevs_lex: Scan.Lexicon,
-  abbrevs_map: Map[String, (String, String)])
+  words_lex: Scan.Lexicon = Scan.Lexicon.empty,
+  words_map: Map[String, String] = Map.empty,
+  abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
+  abbrevs_map: Map[String, (String, String)] = Map.empty)
 {
   /* adding stuff */