equal
deleted
inserted
replaced
104 val caret = text_area.getCaretPosition |
104 val caret = text_area.getCaretPosition |
105 val line = buffer.getLineOfOffset(caret) |
105 val line = buffer.getLineOfOffset(caret) |
106 val start = buffer.getLineStartOffset(line) |
106 val start = buffer.getLineStartOffset(line) |
107 val text = buffer.getSegment(start, caret - start) |
107 val text = buffer.getSegment(start, caret - start) |
108 |
108 |
|
109 val history = PIDE.completion_history.value |
109 val decode = Isabelle_Encoding.is_active(buffer) |
110 val decode = Isabelle_Encoding.is_active(buffer) |
110 syntax.completion.complete(decode, explicit, text) match { |
111 syntax.completion.complete(history, decode, explicit, text) match { |
111 case Some(result) => |
112 case Some(result) => |
112 if (result.unique && result.items.head.immediate && immediate) |
113 if (result.unique && result.items.head.immediate && immediate) |
113 insert(result.items.head) |
114 insert(result.items.head) |
114 else { |
115 else { |
115 val font = |
116 val font = |
121 SwingUtilities.convertPoint(painter, |
122 SwingUtilities.convertPoint(painter, |
122 loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered) |
123 loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered) |
123 |
124 |
124 val completion = |
125 val completion = |
125 new Completion_Popup(layered, loc2, font, result.items) { |
126 new Completion_Popup(layered, loc2, font, result.items) { |
126 override def complete(item: Completion.Item) { insert(item) } |
127 override def complete(item: Completion.Item) { |
|
128 PIDE.completion_history.update(item) |
|
129 insert(item) |
|
130 } |
127 override def propagate(evt: KeyEvent) { |
131 override def propagate(evt: KeyEvent) { |
128 JEdit_Lib.propagate_key(view, evt) |
132 JEdit_Lib.propagate_key(view, evt) |
129 input(evt) |
133 input(evt) |
130 } |
134 } |
131 override def refocus() { text_area.requestFocus } |
135 override def refocus() { text_area.requestFocus } |