# 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}", "`" -> "\\\u0007\\", "`" -> "\\", "`" -> "\\") + List("@{" -> "@{\u0007}", + "`" -> "\\", + "`" -> "\\", + "`" -> "\\\u0007\\") + + private def default_frequency(name: String): Option[Int] = + default_abbrs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2) } final class Completion private(