97 { |
97 { |
98 val view = text_area.getView |
98 val view = text_area.getView |
99 val layered = view.getLayeredPane |
99 val layered = view.getLayeredPane |
100 val buffer = text_area.getBuffer |
100 val buffer = text_area.getBuffer |
101 val painter = text_area.getPainter |
101 val painter = text_area.getPainter |
102 |
102 val caret = text_area.getCaretPosition |
103 if (buffer.isEditable) { |
103 |
|
104 val history = PIDE.completion_history.value |
|
105 val decode = Isabelle_Encoding.is_active(buffer) |
|
106 |
|
107 def open_popup(result: Completion.Result) |
|
108 { |
|
109 val font = |
|
110 painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale")) |
|
111 |
|
112 val loc1 = text_area.offsetToXY(result.range.start) |
|
113 if (loc1 != null) { |
|
114 val loc2 = |
|
115 SwingUtilities.convertPoint(painter, |
|
116 loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered) |
|
117 |
|
118 val completion = |
|
119 new Completion_Popup(layered, loc2, font, result.items) { |
|
120 override def complete(item: Completion.Item) { |
|
121 PIDE.completion_history.update(item) |
|
122 insert(item) |
|
123 } |
|
124 override def propagate(evt: KeyEvent) { |
|
125 JEdit_Lib.propagate_key(view, evt) |
|
126 input(evt) |
|
127 } |
|
128 override def refocus() { text_area.requestFocus } |
|
129 } |
|
130 completion_popup = Some(completion) |
|
131 completion.show_popup() |
|
132 } |
|
133 } |
|
134 |
|
135 def semantic_completion(): Boolean = |
|
136 explicit && { |
|
137 PIDE.document_view(text_area) match { |
|
138 case Some(doc_view) => |
|
139 val rendering = doc_view.get_rendering() |
|
140 rendering.completion_names(JEdit_Lib.stretch_point_range(buffer, caret)) match { |
|
141 case None => false |
|
142 case Some(names) => |
|
143 JEdit_Lib.try_get_text(buffer, names.range) match { |
|
144 case Some(original) => |
|
145 names.complete(history, decode, original) match { |
|
146 case Some(result) if !result.items.isEmpty => |
|
147 open_popup(result) |
|
148 true |
|
149 case _ => false |
|
150 } |
|
151 case None => false |
|
152 } |
|
153 } |
|
154 case _ => false |
|
155 } |
|
156 } |
|
157 |
|
158 def syntax_completion(): Boolean = |
|
159 { |
104 Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match { |
160 Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match { |
105 case Some(syntax) => |
161 case Some(syntax) => |
106 val caret = text_area.getCaretPosition |
|
107 val line = buffer.getLineOfOffset(caret) |
162 val line = buffer.getLineOfOffset(caret) |
108 val start = buffer.getLineStartOffset(line) |
163 val start = buffer.getLineStartOffset(line) |
109 val text = buffer.getSegment(start, caret - start) |
164 val text = buffer.getSegment(start, caret - start) |
110 |
165 |
111 val history = PIDE.completion_history.value |
|
112 val decode = Isabelle_Encoding.is_active(buffer) |
|
113 val context = |
166 val context = |
114 (PIDE.document_view(text_area) match { |
167 (PIDE.document_view(text_area) match { |
115 case None => None |
168 case None => None |
116 case Some(doc_view) => |
169 case Some(doc_view) => |
117 val rendering = doc_view.get_rendering() |
170 val rendering = doc_view.get_rendering() |
118 rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret)) |
171 rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret)) |
119 }) getOrElse syntax.completion_context |
172 }) getOrElse syntax.completion_context |
120 |
173 |
121 syntax.completion.complete(history, decode, explicit, start, text, context) match { |
174 syntax.completion.complete(history, decode, explicit, start, text, context) match { |
122 case Some(result) => |
175 case Some(result) => |
123 if (result.unique && result.items.head.immediate && immediate) |
176 result.items match { |
124 insert(result.items.head) |
177 case List(item) if result.unique && item.immediate && immediate => |
125 else { |
178 insert(item) |
126 val font = |
179 true |
127 painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale")) |
180 case _ :: _ => |
128 |
181 open_popup(result) |
129 val loc1 = text_area.offsetToXY(caret - result.original.length) |
182 true |
130 if (loc1 != null) { |
183 case _ => false |
131 val loc2 = |
|
132 SwingUtilities.convertPoint(painter, |
|
133 loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered) |
|
134 |
|
135 val completion = |
|
136 new Completion_Popup(layered, loc2, font, result.items) { |
|
137 override def complete(item: Completion.Item) { |
|
138 PIDE.completion_history.update(item) |
|
139 insert(item) |
|
140 } |
|
141 override def propagate(evt: KeyEvent) { |
|
142 JEdit_Lib.propagate_key(view, evt) |
|
143 input(evt) |
|
144 } |
|
145 override def refocus() { text_area.requestFocus } |
|
146 } |
|
147 completion_popup = Some(completion) |
|
148 completion.show_popup() |
|
149 } |
|
150 } |
184 } |
151 case None => |
185 case None => false |
152 } |
186 } |
153 case None => |
187 case None => false |
154 } |
188 } |
155 } |
189 } |
|
190 |
|
191 if (buffer.isEditable) |
|
192 semantic_completion() || syntax_completion() |
156 } |
193 } |
157 |
194 |
158 |
195 |
159 /* input key events */ |
196 /* input key events */ |
160 |
197 |