71 } |
76 } |
72 } |
77 } |
73 } |
78 } |
74 } |
79 } |
75 |
80 |
|
81 |
|
82 /* input of key events */ |
|
83 |
76 def input(evt: KeyEvent) |
84 def input(evt: KeyEvent) |
77 { |
85 { |
78 Swing_Thread.require() |
86 Swing_Thread.require() |
79 |
87 |
80 val view = text_area.getView |
88 if (PIDE.options.bool("jedit_completion")) { |
81 val layered = view.getLayeredPane |
89 if (!evt.isConsumed) { |
82 val buffer = text_area.getBuffer |
90 dismissed() |
83 val painter = text_area.getPainter |
91 input_delay.invoke() |
84 |
92 } |
85 if (buffer.isEditable && !evt.isConsumed) { |
93 } |
|
94 else { |
86 dismissed() |
95 dismissed() |
87 |
96 input_delay.revoke() |
88 get_syntax match { |
97 } |
89 case Some(syntax) => |
98 } |
90 val caret = text_area.getCaretPosition |
99 |
91 val result = |
100 private val input_delay = |
92 { |
101 Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) |
93 val line = buffer.getLineOfOffset(caret) |
102 { |
94 val start = buffer.getLineStartOffset(line) |
103 val view = text_area.getView |
95 val text = buffer.getSegment(start, caret - start) |
104 val layered = view.getLayeredPane |
96 |
105 val buffer = text_area.getBuffer |
97 syntax.completion.complete(text) match { |
106 val painter = text_area.getPainter |
98 case Some((word, cs)) => |
107 |
99 val ds = |
108 if (buffer.isEditable) { |
100 (if (Isabelle_Encoding.is_active(buffer)) |
109 get_syntax match { |
101 cs.map(Symbol.decode(_)).sorted |
110 case Some(syntax) => |
102 else cs).filter(_ != word) |
111 val caret = text_area.getCaretPosition |
103 if (ds.isEmpty) None |
112 val result = |
104 else Some((word, ds.map(s => Item(word, s, s)))) |
113 { |
105 case None => None |
114 val line = buffer.getLineOfOffset(caret) |
|
115 val start = buffer.getLineStartOffset(line) |
|
116 val text = buffer.getSegment(start, caret - start) |
|
117 |
|
118 syntax.completion.complete(text) match { |
|
119 case Some((word, cs)) => |
|
120 val ds = |
|
121 (if (Isabelle_Encoding.is_active(buffer)) |
|
122 cs.map(Symbol.decode(_)).sorted |
|
123 else cs).filter(_ != word) |
|
124 if (ds.isEmpty) None |
|
125 else Some((word, ds.map(s => Item(word, s, s)))) |
|
126 case None => None |
|
127 } |
106 } |
128 } |
107 } |
129 result match { |
108 result match { |
130 case Some((original, items)) => |
109 case Some((original, items)) => |
131 val font = |
110 val font = painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale")) |
132 painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale")) |
111 |
133 |
112 val loc1 = text_area.offsetToXY(caret - original.length) |
134 val loc1 = text_area.offsetToXY(caret - original.length) |
113 if (loc1 != null) { |
135 if (loc1 != null) { |
114 val loc2 = |
136 val loc2 = |
115 SwingUtilities.convertPoint(painter, |
137 SwingUtilities.convertPoint(painter, |
116 loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered) |
138 loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered) |
117 val completion = |
139 |
118 new Completion_Popup(layered, loc2, font, items) { |
140 val completion = |
119 override def complete(item: Item) { insert(item) } |
141 new Completion_Popup(layered, loc2, font, items) { |
120 override def propagate(e: KeyEvent) { |
142 override def complete(item: Item) { insert(item) } |
121 JEdit_Lib.propagate_key(view, e) |
143 override def propagate(e: KeyEvent) { |
122 input(e) |
144 JEdit_Lib.propagate_key(view, e) |
|
145 input(e) |
|
146 } |
|
147 override def refocus() { text_area.requestFocus } |
123 } |
148 } |
124 override def refocus() { text_area.requestFocus } |
149 completion_popup = Some(completion) |
125 } |
150 completion.show_popup() |
126 completion_popup = Some(completion) |
151 } |
127 completion.show_popup() |
152 case None => |
128 } |
153 } |
129 case None => |
154 case None => |
130 } |
155 } |
131 case None => |
|
132 } |
156 } |
133 } |
157 } |
134 } |
|
135 } |
158 } |
136 } |
159 } |
137 |
160 |
138 |
161 |
139 class Completion_Popup private( |
162 class Completion_Popup private( |