134 case XML.Elem(Markup(Markup.COMPLETION, _), body) => |
134 case XML.Elem(Markup(Markup.COMPLETION, _), body) => |
135 try { |
135 try { |
136 val (total, names) = |
136 val (total, names) = |
137 { |
137 { |
138 import XML.Decode._ |
138 import XML.Decode._ |
139 pair(int, list(pair(string, string)))(body) |
139 pair(int, list(pair(string, pair(string, string))))(body) |
140 } |
140 } |
141 Some(Names(info.range, total, names)) |
141 Some(Names(info.range, total, names)) |
142 } |
142 } |
143 catch { case _: XML.Error => None } |
143 catch { case _: XML.Error => None } |
144 case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) => |
144 case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) => |
146 case _ => None |
146 case _ => None |
147 } |
147 } |
148 } |
148 } |
149 } |
149 } |
150 |
150 |
151 sealed case class Names(range: Text.Range, total: Int, names: List[(String, String)]) |
151 sealed case class Names( |
|
152 range: Text.Range, total: Int, names: List[(String, (String, String))]) |
152 { |
153 { |
153 def no_completion: Boolean = total == 0 && names.isEmpty |
154 def no_completion: Boolean = total == 0 && names.isEmpty |
154 |
155 |
155 def complete( |
156 def complete( |
156 history: Completion.History, |
157 history: Completion.History, |
157 decode: Boolean, |
158 do_decode: Boolean, |
158 original: String): Option[Completion.Result] = |
159 original: String): Option[Completion.Result] = |
159 { |
160 { |
|
161 def decode(s: String): String = if (do_decode) Symbol.decode(s) else s |
160 val items = |
162 val items = |
161 for { |
163 for { |
162 (xname, name) <- names |
164 (xname, (kind, name)) <- names |
163 xname1 = (if (decode) Symbol.decode(xname) else xname) |
165 xname1 = decode(xname) |
164 if xname1 != original |
166 if xname1 != original |
165 } yield Item(range, original, name, xname1, xname1, 0, true) |
167 (full_name, descr_name) = |
|
168 if (kind == "") (name, quote(decode(name))) |
|
169 else (kind + "." + name, Library.plain_words(kind) + " " + quote(decode(name))) |
|
170 description = xname1 + " (" + descr_name + ")" |
|
171 } yield Item(range, original, full_name, description, xname1, 0, true) |
166 |
172 |
167 if (items.isEmpty) None |
173 if (items.isEmpty) None |
168 else Some(Result(range, original, names.length == 1, items.sorted(history.ordering))) |
174 else Some(Result(range, original, names.length == 1, items.sorted(history.ordering))) |
169 } |
175 } |
170 } |
176 } |
296 |
302 |
297 /* complete */ |
303 /* complete */ |
298 |
304 |
299 def complete( |
305 def complete( |
300 history: Completion.History, |
306 history: Completion.History, |
301 decode: Boolean, |
307 do_decode: Boolean, |
302 explicit: Boolean, |
308 explicit: Boolean, |
303 start: Text.Offset, |
309 start: Text.Offset, |
304 text: CharSequence, |
310 text: CharSequence, |
305 caret: Int, |
311 caret: Int, |
306 extend_word: Boolean, |
312 extend_word: Boolean, |
307 language_context: Completion.Language_Context): Option[Completion.Result] = |
313 language_context: Completion.Language_Context): Option[Completion.Result] = |
308 { |
314 { |
|
315 def decode(s: String): String = if (do_decode) Symbol.decode(s) else s |
309 val length = text.length |
316 val length = text.length |
310 |
317 |
311 val abbrevs_result = |
318 val abbrevs_result = |
312 { |
319 { |
313 val reverse_in = new Library.Reverse(text.subSequence(0, caret)) |
320 val reverse_in = new Library.Reverse(text.subSequence(0, caret)) |
354 } |
361 } |
355 |
362 |
356 words_result match { |
363 words_result match { |
357 case Some(((word, cs), end)) => |
364 case Some(((word, cs), end)) => |
358 val range = Text.Range(- word.length, 0) + end + start |
365 val range = Text.Range(- word.length, 0) + end + start |
359 val ds = (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word) |
366 val ds = cs.map(decode(_)).filter(_ != word) |
360 if (ds.isEmpty) None |
367 if (ds.isEmpty) None |
361 else { |
368 else { |
362 val immediate = |
369 val immediate = |
363 !Completion.Word_Parsers.is_word(word) && |
370 !Completion.Word_Parsers.is_word(word) && |
364 Character.codePointCount(word, 0, word.length) > 1 |
371 Character.codePointCount(word, 0, word.length) > 1 |
365 val items = |
372 val items = |
366 ds.map(s => { |
373 for { (name, name1) <- cs zip ds } |
|
374 yield { |
367 val (s1, s2) = |
375 val (s1, s2) = |
368 space_explode(Completion.caret_indicator, s) match { |
376 space_explode(Completion.caret_indicator, name1) match { |
369 case List(s1, s2) => (s1, s2) |
377 case List(s1, s2) => (s1, s2) |
370 case _ => (s, "") |
378 case _ => (name1, "") |
371 } |
379 } |
372 Completion.Item(range, word, s, s, s1 + s2, - s2.length, explicit || immediate) |
380 val description = |
373 }) |
381 if (keywords(name)) name1 + " (keyword)" |
|
382 else if (Symbol.names.isDefinedAt(name) && name != name1) |
|
383 name1 + " (symbol " + quote(name) + ")" |
|
384 else name1 |
|
385 Completion.Item( |
|
386 range, word, name1, description, s1 + s2, - s2.length, explicit || immediate) |
|
387 } |
374 Some(Completion.Result(range, word, cs.length == 1, items.sorted(history.ordering))) |
388 Some(Completion.Result(range, word, cs.length == 1, items.sorted(history.ordering))) |
375 } |
389 } |
376 case None => None |
390 case None => None |
377 } |
391 } |
378 } |
392 } |