# HG changeset patch
# User wenzelm
# Date 1330024999 -3600
# Node ID 630542c79604b4fc9da7eb054313658322a70a4f
# Parent  dc4c720920881365ad0f3a16cd6764e0ae35cfbf
tuned;

diff -r dc4c72092088 -r 630542c79604 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 */