src/Tools/jEdit/src/completion_popup.scala
changeset 53337 b3817a0e3211
parent 53325 ffabc0083786
child 53397 b179cdfa9d82
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 22:22:07 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Aug 30 23:38:18 2013 +0200
     1.3 @@ -106,8 +106,9 @@
     1.4              val start = buffer.getLineStartOffset(line)
     1.5              val text = buffer.getSegment(start, caret - start)
     1.6  
     1.7 +            val history = PIDE.completion_history.value
     1.8              val decode = Isabelle_Encoding.is_active(buffer)
     1.9 -            syntax.completion.complete(decode, explicit, text) match {
    1.10 +            syntax.completion.complete(history, decode, explicit, text) match {
    1.11                case Some(result) =>
    1.12                  if (result.unique && result.items.head.immediate && immediate)
    1.13                    insert(result.items.head)
    1.14 @@ -123,7 +124,10 @@
    1.15  
    1.16                      val completion =
    1.17                        new Completion_Popup(layered, loc2, font, result.items) {
    1.18 -                        override def complete(item: Completion.Item) { insert(item) }
    1.19 +                        override def complete(item: Completion.Item) {
    1.20 +                          PIDE.completion_history.update(item)
    1.21 +                          insert(item)
    1.22 +                        }
    1.23                          override def propagate(evt: KeyEvent) {
    1.24                            JEdit_Lib.propagate_key(view, evt)
    1.25                            input(evt)