# HG changeset patch # User wenzelm # Date 1377898698 -7200 # Node ID b3817a0e32112ebeea5f4a302263d0fccddd39f6 # Parent b3bf6d72fea55d5c2550ee003dae5ce53c6e3eb2 sort items according to persistent history of frequency of use; diff -r b3bf6d72fea5 -r b3817a0e3211 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Fri Aug 30 22:22:07 2013 +0200 +++ b/src/Pure/General/symbol.scala Fri Aug 30 23:38:18 2013 +0200 @@ -388,6 +388,9 @@ def decode(text: String): String = symbols.decode(text) def encode(text: String): String = symbols.encode(text) + def decode_string: XML.Decode.T[String] = (x => decode(XML.Decode.string(x))) + def encode_string: XML.Encode.T[String] = (x => XML.Encode.string(encode(x))) + def decode_strict(text: String): String = { val decoded = decode(text) diff -r b3bf6d72fea5 -r b3817a0e3211 src/Pure/Isar/completion.scala --- a/src/Pure/Isar/completion.scala Fri Aug 30 22:22:07 2013 +0200 +++ b/src/Pure/Isar/completion.scala Fri Aug 30 23:38:18 2013 +0200 @@ -6,7 +6,9 @@ package isabelle +import scala.collection.immutable.SortedMap import scala.util.parsing.combinator.RegexParsers +import scala.math.Ordering object Completion @@ -29,6 +31,88 @@ def init(): Completion = empty.add_symbols() + /** persistent history **/ + + private val COMPLETION_HISTORY = Path.explode("$ISABELLE_HOME_USER/etc/completion_history") + + object History + { + val empty: History = new History() + + def load(): History = + { + def ignore_error(msg: String): Unit = + java.lang.System.err.println("### Ignoring bad content of file " + COMPLETION_HISTORY + + (if (msg == "") "" else "\n" + msg)) + + val content = + if (COMPLETION_HISTORY.is_file) { + try { + import XML.Decode._ + list(pair(Symbol.decode_string, int))( + YXML.parse_body(File.read(COMPLETION_HISTORY))) + } + catch { + case ERROR(msg) => ignore_error(msg); Nil + case _: XML.Error => ignore_error(""); Nil + } + } + else Nil + (empty /: content)(_ + _) + } + } + + final class History private(rep: SortedMap[String, Int] = SortedMap.empty) + { + override def toString: String = rep.mkString("Completion.History(", ",", ")") + + def frequency(name: String): Int = rep.getOrElse(name, 0) + + def + (entry: (String, Int)): History = + { + val (name, freq) = entry + new History(rep + (name -> (frequency(name) + freq))) + } + + def ordering: Ordering[Item] = + new Ordering[Item] { + def compare(item1: Item, item2: Item): Int = + { + frequency(item1.replacement) compare frequency(item2.replacement) match { + case 0 => item1.replacement compare item2.replacement + case ord => - ord + } + } + } + + def save() + { + Isabelle_System.mkdirs(COMPLETION_HISTORY.dir) + File.write_backup(COMPLETION_HISTORY, + { + import XML.Encode._ + YXML.string_of_body(list(pair(Symbol.encode_string, int))(rep.toList)) + }) + } + } + + class History_Variable + { + private var history = History.empty + def value: History = synchronized { history } + + def load() + { + val h = History.load() + synchronized { history = h } + } + + def update(item: Item, freq: Int = 1): Unit = synchronized { + history = history + (item.replacement -> freq) + } + } + + /** word completion **/ private val word_regex = "[a-zA-Z0-9_']+".r @@ -94,7 +178,11 @@ /* complete */ - def complete(decode: Boolean, explicit: Boolean, line: CharSequence): Option[Completion.Result] = + def complete( + history: Completion.History, + decode: Boolean, + explicit: Boolean, + line: CharSequence): Option[Completion.Result] = { val raw_result = abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match { @@ -109,21 +197,22 @@ case Some(word) => words_lex.completions(word).map(words_map.get_list(_)).flatten match { case Nil => None - case cs => Some(word, cs.sorted) + case cs => Some(word, cs) } case None => None } } raw_result match { case Some((word, cs)) => - val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word) + val ds = + (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word) if (ds.isEmpty) None else { val immediate = !Completion.is_word(word) && Character.codePointCount(word, 0, word.length) > 1 val items = ds.map(s => Completion.Item(word, s, s, explicit || immediate)) - Some(Completion.Result(word, cs.length == 1, items)) + Some(Completion.Result(word, cs.length == 1, items.sorted(history.ordering))) } case None => None } diff -r b3bf6d72fea5 -r b3817a0e3211 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Fri Aug 30 22:22:07 2013 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Fri Aug 30 23:38:18 2013 +0200 @@ -106,8 +106,9 @@ val start = buffer.getLineStartOffset(line) val text = buffer.getSegment(start, caret - start) + val history = PIDE.completion_history.value val decode = Isabelle_Encoding.is_active(buffer) - syntax.completion.complete(decode, explicit, text) match { + syntax.completion.complete(history, decode, explicit, text) match { case Some(result) => if (result.unique && result.items.head.immediate && immediate) insert(result.items.head) @@ -123,7 +124,10 @@ val completion = new Completion_Popup(layered, loc2, font, result.items) { - override def complete(item: Completion.Item) { insert(item) } + override def complete(item: Completion.Item) { + PIDE.completion_history.update(item) + insert(item) + } override def propagate(evt: KeyEvent) { JEdit_Lib.propagate_key(view, evt) input(evt) diff -r b3bf6d72fea5 -r b3817a0e3211 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Fri Aug 30 22:22:07 2013 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Fri Aug 30 23:38:18 2013 +0200 @@ -28,6 +28,7 @@ /* plugin instance */ val options = new JEdit_Options + val completion_history = new Completion.History_Variable @volatile var startup_failure: Option[Throwable] = None @volatile var startup_notified = false @@ -304,6 +305,7 @@ val init_options = Options.init() Swing_Thread.now { PIDE.options.update(init_options) } + PIDE.completion_history.load() if (Platform.is_macos && PIDE.options.bool("jedit_mac_adapter")) OSX_Adapter.set_quit_handler(this, this.getClass.getDeclaredMethod("handle_quit")) @@ -336,8 +338,10 @@ { JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _) - if (PIDE.startup_failure.isEmpty) + if (PIDE.startup_failure.isEmpty) { PIDE.options.value.save_prefs() + PIDE.completion_history.value.save() + } PIDE.session.phase_changed -= session_manager PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)