--- 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)
--- 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
}
--- 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)
--- 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)