src/Pure/General/completion.scala

   /* abbreviations */
 
   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(
   keywords: Map[String, Boolean] = Map.empty,
   words_lex: Scan.Lexicon = Scan.Lexicon.empty,

     val symbol_abbrs =
       (for ((x, y) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(y))
         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(
       keywords,
       words_lex ++ words.map(_._1),

           abbrevs match {
             case Nil => None
             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
           }
         case _ => None
       }