# HG changeset patch
# User wenzelm
# Date 1446906206 -3600
# Node ID 2e52df0cd8eea4591eeb87295394123522a7a70a
# Parent  ed4dad8823a44ed814bb38af553da539a6a94bb0
tuned;

diff -r ed4dad8823a4 -r 2e52df0cd8ee src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Sat Nov 07 13:13:23 2015 +0100
+++ b/src/Pure/General/completion.scala	Sat Nov 07 15:23:26 2015 +0100
@@ -251,7 +251,7 @@
 
     private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
     private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
-    private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
+    private def reverse_escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
 
     private val word_regex = "[a-zA-Z0-9_'.]+".r
     private def word: Parser[String] = word_regex
@@ -275,7 +275,7 @@
       val parse_word = if (explicit) word else word3
       val reverse_in = new Library.Reverse(in)
       val parser =
-        (reverse_symbol | reverse_symb | escape) ^^ (x => (x.reverse, "")) |
+        (reverse_symbol | reverse_symb | reverse_escape) ^^ (x => (x.reverse, "")) |
         underscores ~ parse_word ~ opt("?") ^^
         { case x ~ y ~ z => (z.getOrElse("") + y.reverse, x) }
       parse(parser, reverse_in) match {
@@ -354,17 +354,18 @@
   private def add_symbols(): Completion =
   {
     val words =
-      (for ((x, _) <- Symbol.names.toList) yield (x, x)) :::
-      (for ((x, y) <- Symbol.names.toList) yield ("\\" + y, x)) :::
-      (for ((x, y) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(y)) yield (y, x))
+      (for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
+      (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym)) :::
+      (for ((sym, abbr) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(abbr))
+        yield (abbr, sym))
 
     val symbol_abbrs =
-      (for ((x, y) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(y))
-        yield (y, x)).toList
+      (for ((sym, abbr) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(abbr))
+        yield (abbr, sym)).toList
 
     val abbrs =
-      for ((a, b) <- symbol_abbrs ::: Completion.default_abbrs)
-        yield (a.reverse, (a, b))
+      for ((abbr, sym) <- symbol_abbrs ::: Completion.default_abbrs)
+        yield (abbr.reverse, (abbr, sym))
 
     new Completion(
       keywords,
@@ -393,18 +394,18 @@
     {
       val reverse_in = new Library.Reverse(text.subSequence(0, caret))
       Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), reverse_in) match {
-        case Scan.Parsers.Success(reverse_a, _) =>
-          val abbrevs = abbrevs_map.get_list(reverse_a)
+        case Scan.Parsers.Success(reverse_abbr, _) =>
+          val abbrevs = abbrevs_map.get_list(reverse_abbr)
           abbrevs match {
             case Nil => None
-            case (a, _) :: _ =>
+            case (abbr, _) :: _ =>
               val ok =
-                if (a == Completion.antiquote) language_context.antiquotes
+                if (abbr == Completion.antiquote) language_context.antiquotes
                 else
                   language_context.symbols ||
-                  Completion.default_abbrs.exists(_._1 == a) ||
-                  Completion.Word_Parsers.is_symbol(a)
-              if (ok) Some((a, abbrevs))
+                  Completion.default_abbrs.exists(_._1 == abbr) ||
+                  Completion.Word_Parsers.is_symbol(abbr)
+              if (ok) Some((abbr, abbrevs))
               else None
           }
         case _ => None