# HG changeset patch
# User wenzelm
# Date 1377857393 -7200
# Node ID ec45115483044fd401faa692b2cfeb54ebea8110
# Parent  dea84641ca353270d1d91bb42ba853cd7eb6c802
allow multiple entries;

diff -r dea84641ca35 -r ec4511548304 src/Pure/Isar/completion.scala
--- a/src/Pure/Isar/completion.scala	Fri Aug 30 11:41:43 2013 +0200
+++ b/src/Pure/Isar/completion.scala	Fri Aug 30 12:09:53 2013 +0200
@@ -54,9 +54,9 @@
 
 final class Completion private(
   words_lex: Scan.Lexicon = Scan.Lexicon.empty,
-  words_map: Map[String, String] = Map.empty,
+  words_map: Multi_Map[String, String] = Multi_Map.empty,
   abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
-  abbrevs_map: Map[String, (String, String)] = Map.empty)
+  abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
 {
   /* adding stuff */
 
@@ -95,12 +95,15 @@
     val raw_result =
       abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
         case abbrevs_lex.Success(reverse_a, _) =>
-          val (word, c) = abbrevs_map(reverse_a)
-          Some(word, List(c))
+          val abbrevs = abbrevs_map.get_list(reverse_a)
+          abbrevs match {
+            case Nil => None
+            case (a, _) :: _ => Some((a, abbrevs.map(_._2)))
+          }
         case _ =>
           Completion.Parse.read(line) match {
             case Some(word) =>
-              words_lex.completions(word).map(words_map(_)) match {
+              words_lex.completions(word).map(words_map.get_list(_)).flatten match {
                 case Nil => None
                 case cs => Some(word, cs.sorted)
               }