sort items according to persistent history of frequency of use;
authorwenzelm
Fri Aug 30 23:38:18 2013 +0200 (2013-08-30 ago)
changeset 53337b3817a0e3211
parent 53336 b3bf6d72fea5
child 53338 69a0bdfc7fa5
sort items according to persistent history of frequency of use;
src/Pure/General/symbol.scala
src/Pure/Isar/completion.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/General/symbol.scala	Fri Aug 30 22:22:07 2013 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Fri Aug 30 23:38:18 2013 +0200
     1.3 @@ -388,6 +388,9 @@
     1.4    def decode(text: String): String = symbols.decode(text)
     1.5    def encode(text: String): String = symbols.encode(text)
     1.6  
     1.7 +  def decode_string: XML.Decode.T[String] = (x => decode(XML.Decode.string(x)))
     1.8 +  def encode_string: XML.Encode.T[String] = (x => XML.Encode.string(encode(x)))
     1.9 +
    1.10    def decode_strict(text: String): String =
    1.11    {
    1.12      val decoded = decode(text)
     2.1 --- a/src/Pure/Isar/completion.scala	Fri Aug 30 22:22:07 2013 +0200
     2.2 +++ b/src/Pure/Isar/completion.scala	Fri Aug 30 23:38:18 2013 +0200
     2.3 @@ -6,7 +6,9 @@
     2.4  
     2.5  package isabelle
     2.6  
     2.7 +import scala.collection.immutable.SortedMap
     2.8  import scala.util.parsing.combinator.RegexParsers
     2.9 +import scala.math.Ordering
    2.10  
    2.11  
    2.12  object Completion
    2.13 @@ -29,6 +31,88 @@
    2.14    def init(): Completion = empty.add_symbols()
    2.15  
    2.16  
    2.17 +  /** persistent history **/
    2.18 +
    2.19 +  private val COMPLETION_HISTORY = Path.explode("$ISABELLE_HOME_USER/etc/completion_history")
    2.20 +
    2.21 +  object History
    2.22 +  {
    2.23 +    val empty: History = new History()
    2.24 +
    2.25 +    def load(): History =
    2.26 +    {
    2.27 +      def ignore_error(msg: String): Unit =
    2.28 +        java.lang.System.err.println("### Ignoring bad content of file " + COMPLETION_HISTORY +
    2.29 +          (if (msg == "") "" else "\n" + msg))
    2.30 +
    2.31 +      val content =
    2.32 +        if (COMPLETION_HISTORY.is_file) {
    2.33 +          try {
    2.34 +            import XML.Decode._
    2.35 +            list(pair(Symbol.decode_string, int))(
    2.36 +              YXML.parse_body(File.read(COMPLETION_HISTORY)))
    2.37 +          }
    2.38 +          catch {
    2.39 +            case ERROR(msg) => ignore_error(msg); Nil
    2.40 +            case _: XML.Error => ignore_error(""); Nil
    2.41 +          }
    2.42 +        }
    2.43 +        else Nil
    2.44 +      (empty /: content)(_ + _)
    2.45 +    }
    2.46 +  }
    2.47 +
    2.48 +  final class History private(rep: SortedMap[String, Int] = SortedMap.empty)
    2.49 +  {
    2.50 +    override def toString: String = rep.mkString("Completion.History(", ",", ")")
    2.51 +
    2.52 +    def frequency(name: String): Int = rep.getOrElse(name, 0)
    2.53 +
    2.54 +    def + (entry: (String, Int)): History =
    2.55 +    {
    2.56 +      val (name, freq) = entry
    2.57 +      new History(rep + (name -> (frequency(name) + freq)))
    2.58 +    }
    2.59 +
    2.60 +    def ordering: Ordering[Item] =
    2.61 +      new Ordering[Item] {
    2.62 +        def compare(item1: Item, item2: Item): Int =
    2.63 +        {
    2.64 +          frequency(item1.replacement) compare frequency(item2.replacement) match {
    2.65 +            case 0 => item1.replacement compare item2.replacement
    2.66 +            case ord => - ord
    2.67 +          }
    2.68 +        }
    2.69 +      }
    2.70 +
    2.71 +    def save()
    2.72 +    {
    2.73 +      Isabelle_System.mkdirs(COMPLETION_HISTORY.dir)
    2.74 +      File.write_backup(COMPLETION_HISTORY,
    2.75 +        {
    2.76 +          import XML.Encode._
    2.77 +          YXML.string_of_body(list(pair(Symbol.encode_string, int))(rep.toList))
    2.78 +        })
    2.79 +    }
    2.80 +  }
    2.81 +
    2.82 +  class History_Variable
    2.83 +  {
    2.84 +    private var history = History.empty
    2.85 +    def value: History = synchronized { history }
    2.86 +
    2.87 +    def load()
    2.88 +    {
    2.89 +      val h = History.load()
    2.90 +      synchronized { history = h }
    2.91 +    }
    2.92 +
    2.93 +    def update(item: Item, freq: Int = 1): Unit = synchronized {
    2.94 +      history = history + (item.replacement -> freq)
    2.95 +    }
    2.96 +  }
    2.97 +
    2.98 +
    2.99    /** word completion **/
   2.100  
   2.101    private val word_regex = "[a-zA-Z0-9_']+".r
   2.102 @@ -94,7 +178,11 @@
   2.103  
   2.104    /* complete */
   2.105  
   2.106 -  def complete(decode: Boolean, explicit: Boolean, line: CharSequence): Option[Completion.Result] =
   2.107 +  def complete(
   2.108 +    history: Completion.History,
   2.109 +    decode: Boolean,
   2.110 +    explicit: Boolean,
   2.111 +    line: CharSequence): Option[Completion.Result] =
   2.112    {
   2.113      val raw_result =
   2.114        abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
   2.115 @@ -109,21 +197,22 @@
   2.116              case Some(word) =>
   2.117                words_lex.completions(word).map(words_map.get_list(_)).flatten match {
   2.118                  case Nil => None
   2.119 -                case cs => Some(word, cs.sorted)
   2.120 +                case cs => Some(word, cs)
   2.121                }
   2.122              case None => None
   2.123            }
   2.124        }
   2.125      raw_result match {
   2.126        case Some((word, cs)) =>
   2.127 -        val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word)
   2.128 +        val ds =
   2.129 +          (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word)
   2.130          if (ds.isEmpty) None
   2.131          else {
   2.132            val immediate =
   2.133              !Completion.is_word(word) &&
   2.134              Character.codePointCount(word, 0, word.length) > 1
   2.135            val items = ds.map(s => Completion.Item(word, s, s, explicit || immediate))
   2.136 -          Some(Completion.Result(word, cs.length == 1, items))
   2.137 +          Some(Completion.Result(word, cs.length == 1, items.sorted(history.ordering)))
   2.138          }
   2.139        case None => None
   2.140      }
     3.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 22:22:07 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 23:38:18 2013 +0200
     3.3 @@ -106,8 +106,9 @@
     3.4              val start = buffer.getLineStartOffset(line)
     3.5              val text = buffer.getSegment(start, caret - start)
     3.6  
     3.7 +            val history = PIDE.completion_history.value
     3.8              val decode = Isabelle_Encoding.is_active(buffer)
     3.9 -            syntax.completion.complete(decode, explicit, text) match {
    3.10 +            syntax.completion.complete(history, decode, explicit, text) match {
    3.11                case Some(result) =>
    3.12                  if (result.unique && result.items.head.immediate && immediate)
    3.13                    insert(result.items.head)
    3.14 @@ -123,7 +124,10 @@
    3.15  
    3.16                      val completion =
    3.17                        new Completion_Popup(layered, loc2, font, result.items) {
    3.18 -                        override def complete(item: Completion.Item) { insert(item) }
    3.19 +                        override def complete(item: Completion.Item) {
    3.20 +                          PIDE.completion_history.update(item)
    3.21 +                          insert(item)
    3.22 +                        }
    3.23                          override def propagate(evt: KeyEvent) {
    3.24                            JEdit_Lib.propagate_key(view, evt)
    3.25                            input(evt)
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Aug 30 22:22:07 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Aug 30 23:38:18 2013 +0200
     4.3 @@ -28,6 +28,7 @@
     4.4    /* plugin instance */
     4.5  
     4.6    val options = new JEdit_Options
     4.7 +  val completion_history = new Completion.History_Variable
     4.8  
     4.9    @volatile var startup_failure: Option[Throwable] = None
    4.10    @volatile var startup_notified = false
    4.11 @@ -304,6 +305,7 @@
    4.12  
    4.13        val init_options = Options.init()
    4.14        Swing_Thread.now { PIDE.options.update(init_options)  }
    4.15 +      PIDE.completion_history.load()
    4.16  
    4.17        if (Platform.is_macos && PIDE.options.bool("jedit_mac_adapter"))
    4.18          OSX_Adapter.set_quit_handler(this, this.getClass.getDeclaredMethod("handle_quit"))
    4.19 @@ -336,8 +338,10 @@
    4.20    {
    4.21      JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
    4.22  
    4.23 -    if (PIDE.startup_failure.isEmpty)
    4.24 +    if (PIDE.startup_failure.isEmpty) {
    4.25        PIDE.options.value.save_prefs()
    4.26 +      PIDE.completion_history.value.save()
    4.27 +    }
    4.28  
    4.29      PIDE.session.phase_changed -= session_manager
    4.30      PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)