src/Pure/General/completion.scala
changeset 56591 1a59587f46ec
parent 56564 94c55cc73747
child 56599 c4424d8c890f
--- a/src/Pure/General/completion.scala	Tue Apr 15 16:44:06 2014 +0200
+++ b/src/Pure/General/completion.scala	Tue Apr 15 19:11:34 2014 +0200
@@ -267,7 +267,7 @@
   private val caret_indicator = '\007'
   private val antiquote = "@{"
   private val default_abbrs =
-    Map("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>")
+    List("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>", "`" -> "\\<open>", "`" -> "\\<close>")
 }
 
 final class Completion private(
@@ -309,7 +309,7 @@
         yield (y, x)).toList
 
     val abbrs =
-      for ((a, b) <- symbol_abbrs ::: Completion.default_abbrs.toList)
+      for ((a, b) <- symbol_abbrs ::: Completion.default_abbrs)
         yield (a.reverse, (a, b))
 
     new Completion(
@@ -347,7 +347,7 @@
             case (a, _) :: _ =>
               val ok =
                 if (a == Completion.antiquote) language_context.antiquotes
-                else language_context.symbols || Completion.default_abbrs.isDefinedAt(a)
+                else language_context.symbols || Completion.default_abbrs.exists(_._1 == a)
               if (ok) Some(((a, abbrevs), caret))
               else None
           }