# HG changeset patch
# User wenzelm
# Date 1399387284 -7200
# Node ID a5d082a851248dbef4ae82125ba251d2099c2479
# Parent  4e9d2eab9cfa7a0a08e5c5673f36c76414bb3694
hardwired default_frequency to avoid fluctuation of popup content;

diff -r 4e9d2eab9cfa -r a5d082a85124 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Tue May 06 16:16:38 2014 +0200
+++ b/src/Pure/General/completion.scala	Tue May 06 16:41:24 2014 +0200
@@ -86,7 +86,9 @@
   {
     override def toString: String = rep.mkString("Completion.History(", ",", ")")
 
-    def frequency(name: String): Int = rep.getOrElse(name, 0)
+    def frequency(name: String): Int =
+      default_frequency(Symbol.encode(name)) getOrElse
+      rep.getOrElse(name, 0)
 
     def + (entry: (String, Int)): History =
     {
@@ -268,8 +270,15 @@
 
   private val caret_indicator = '\u0007'
   private val antiquote = "@{"
+
   private val default_abbrs =
-    List("@{" -> "@{\u0007}", "`" -> "\\<open>\u0007\\<close>", "`" -> "\\<open>", "`" -> "\\<close>")
+    List("@{" -> "@{\u0007}",
+      "`" -> "\\<close>",
+      "`" -> "\\<open>",
+      "`" -> "\\<open>\u0007\\<close>")
+
+  private def default_frequency(name: String): Option[Int] =
+    default_abbrs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)
 }
 
 final class Completion private(