author | wenzelm |
Sat, 08 Mar 2014 13:49:01 +0100 | |
changeset 55996 | 13a7d9661ffc |
parent 55994 | 1c42ebdb3a58 |
child 56001 | 2df1e7bca361 |
permissions | -rw-r--r-- |
55673
0286219c1261
clarified module location (again, see 763d35697338);
wenzelm
parents:
55666
diff
changeset
|
1 |
/* Title: Pure/General/completion.scala |
31763 | 2 |
Author: Makarius |
3 |
||
55687 | 4 |
Semantic completion within the formal context (reported names). |
55674 | 5 |
Syntactic completion of keywords and symbols, with abbreviations |
55992 | 6 |
(based on language context). |
7 |
*/ |
|
31763 | 8 |
|
9 |
package isabelle |
|
10 |
||
55618 | 11 |
|
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
12 |
import scala.collection.immutable.SortedMap |
31763 | 13 |
import scala.util.parsing.combinator.RegexParsers |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
14 |
import scala.math.Ordering |
31763 | 15 |
|
16 |
||
46624 | 17 |
object Completion |
31763 | 18 |
{ |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
19 |
/** completion result **/ |
53275 | 20 |
|
53296
65c60c782da5
less aggressive immediate completion, based on input and text;
wenzelm
parents:
53295
diff
changeset
|
21 |
sealed case class Item( |
55692
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55687
diff
changeset
|
22 |
range: Text.Range, |
53296
65c60c782da5
less aggressive immediate completion, based on input and text;
wenzelm
parents:
53295
diff
changeset
|
23 |
original: String, |
55666 | 24 |
name: String, |
55978 | 25 |
description: List[String], |
53296
65c60c782da5
less aggressive immediate completion, based on input and text;
wenzelm
parents:
53295
diff
changeset
|
26 |
replacement: String, |
55666 | 27 |
move: Int, |
53296
65c60c782da5
less aggressive immediate completion, based on input and text;
wenzelm
parents:
53295
diff
changeset
|
28 |
immediate: Boolean) |
53275 | 29 |
|
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55813
diff
changeset
|
30 |
object Result |
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55813
diff
changeset
|
31 |
{ |
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55813
diff
changeset
|
32 |
def empty(range: Text.Range): Result = Result(range, "", false, Nil) |
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55813
diff
changeset
|
33 |
} |
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55813
diff
changeset
|
34 |
|
55693
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
35 |
sealed case class Result( |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
36 |
range: Text.Range, |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
37 |
original: String, |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
38 |
unique: Boolean, |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
39 |
items: List[Item]) |
53325
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53324
diff
changeset
|
40 |
|
53275 | 41 |
|
46624 | 42 |
|
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
43 |
/** persistent history **/ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
44 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
45 |
private val COMPLETION_HISTORY = Path.explode("$ISABELLE_HOME_USER/etc/completion_history") |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
46 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
47 |
object History |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
48 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
49 |
val empty: History = new History() |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
50 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
51 |
def load(): History = |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
52 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
53 |
def ignore_error(msg: String): Unit = |
55618 | 54 |
System.err.println("### Ignoring bad content of file " + COMPLETION_HISTORY + |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
55 |
(if (msg == "") "" else "\n" + msg)) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
56 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
57 |
val content = |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
58 |
if (COMPLETION_HISTORY.is_file) { |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
59 |
try { |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
60 |
import XML.Decode._ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
61 |
list(pair(Symbol.decode_string, int))( |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
62 |
YXML.parse_body(File.read(COMPLETION_HISTORY))) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
63 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
64 |
catch { |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
65 |
case ERROR(msg) => ignore_error(msg); Nil |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
66 |
case _: XML.Error => ignore_error(""); Nil |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
67 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
68 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
69 |
else Nil |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
70 |
(empty /: content)(_ + _) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
71 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
72 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
73 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
74 |
final class History private(rep: SortedMap[String, Int] = SortedMap.empty) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
75 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
76 |
override def toString: String = rep.mkString("Completion.History(", ",", ")") |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
77 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
78 |
def frequency(name: String): Int = rep.getOrElse(name, 0) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
79 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
80 |
def + (entry: (String, Int)): History = |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
81 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
82 |
val (name, freq) = entry |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
83 |
new History(rep + (name -> (frequency(name) + freq))) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
84 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
85 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
86 |
def ordering: Ordering[Item] = |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
87 |
new Ordering[Item] { |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
88 |
def compare(item1: Item, item2: Item): Int = |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
89 |
{ |
55666 | 90 |
frequency(item1.name) compare frequency(item2.name) match { |
91 |
case 0 => item1.name compare item2.name |
|
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
92 |
case ord => - ord |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
93 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
94 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
95 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
96 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
97 |
def save() |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
98 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
99 |
Isabelle_System.mkdirs(COMPLETION_HISTORY.dir) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
100 |
File.write_backup(COMPLETION_HISTORY, |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
101 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
102 |
import XML.Encode._ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
103 |
YXML.string_of_body(list(pair(Symbol.encode_string, int))(rep.toList)) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
104 |
}) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
105 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
106 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
107 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
108 |
class History_Variable |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
109 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
110 |
private var history = History.empty |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
111 |
def value: History = synchronized { history } |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
112 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
113 |
def load() |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
114 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
115 |
val h = History.load() |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
116 |
synchronized { history = h } |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
117 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
118 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
119 |
def update(item: Item, freq: Int = 1): Unit = synchronized { |
55666 | 120 |
history = history + (item.name -> freq) |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
121 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
122 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
123 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
124 |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
125 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
126 |
/** semantic completion **/ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
127 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
128 |
object Names |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
129 |
{ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
130 |
object Info |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
131 |
{ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
132 |
def unapply(info: Text.Markup): Option[Names] = |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
133 |
info.info match { |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
134 |
case XML.Elem(Markup(Markup.COMPLETION, _), body) => |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
135 |
try { |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
136 |
val (total, names) = |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
137 |
{ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
138 |
import XML.Decode._ |
55977 | 139 |
pair(int, list(pair(string, pair(string, string))))(body) |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
140 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
141 |
Some(Names(info.range, total, names)) |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
142 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
143 |
catch { case _: XML.Error => None } |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55813
diff
changeset
|
144 |
case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) => |
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55813
diff
changeset
|
145 |
Some(Names(info.range, 0, Nil)) |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
146 |
case _ => None |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
147 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
148 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
149 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
150 |
|
55977 | 151 |
sealed case class Names( |
152 |
range: Text.Range, total: Int, names: List[(String, (String, String))]) |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
153 |
{ |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55813
diff
changeset
|
154 |
def no_completion: Boolean = total == 0 && names.isEmpty |
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55813
diff
changeset
|
155 |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
156 |
def complete( |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
157 |
history: Completion.History, |
55977 | 158 |
do_decode: Boolean, |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
159 |
original: String): Option[Completion.Result] = |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
160 |
{ |
55977 | 161 |
def decode(s: String): String = if (do_decode) Symbol.decode(s) else s |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
162 |
val items = |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
163 |
for { |
55977 | 164 |
(xname, (kind, name)) <- names |
165 |
xname1 = decode(xname) |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
166 |
if xname1 != original |
55977 | 167 |
(full_name, descr_name) = |
168 |
if (kind == "") (name, quote(decode(name))) |
|
169 |
else (kind + "." + name, Library.plain_words(kind) + " " + quote(decode(name))) |
|
55978 | 170 |
description = List(xname1, "(" + descr_name + ")") |
55977 | 171 |
} yield Item(range, original, full_name, description, xname1, 0, true) |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
172 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
173 |
if (items.isEmpty) None |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
174 |
else Some(Result(range, original, names.length == 1, items.sorted(history.ordering))) |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
175 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
176 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
177 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
178 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
179 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
180 |
/** syntactic completion **/ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
181 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
182 |
/* language context */ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
183 |
|
55749 | 184 |
object Language_Context |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
185 |
{ |
55749 | 186 |
val outer = Language_Context("", true, false) |
187 |
val inner = Language_Context(Markup.Language.UNKNOWN, true, false) |
|
188 |
val ML_outer = Language_Context(Markup.Language.ML, false, true) |
|
189 |
val ML_inner = Language_Context(Markup.Language.ML, true, false) |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
190 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
191 |
|
55749 | 192 |
sealed case class Language_Context(language: String, symbols: Boolean, antiquotes: Boolean) |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
193 |
{ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
194 |
def is_outer: Boolean = language == "" |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
195 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
196 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
197 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
198 |
/* init */ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
199 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
200 |
val empty: Completion = new Completion() |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
201 |
def init(): Completion = empty.add_symbols() |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
202 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
203 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
204 |
/* word parsers */ |
31763 | 205 |
|
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
206 |
private object Word_Parsers extends RegexParsers |
31763 | 207 |
{ |
208 |
override val whiteSpace = "".r |
|
209 |
||
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
210 |
private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
211 |
private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
212 |
private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
213 |
|
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
214 |
private val word_regex = "[a-zA-Z0-9_']+".r |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
215 |
private def word: Parser[String] = word_regex |
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
216 |
private def word3: Parser[String] = "[a-zA-Z0-9_']{3,}".r |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
217 |
private def underscores: Parser[String] = "_*".r |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
218 |
|
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
219 |
def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
220 |
def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) |
31763 | 221 |
|
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
222 |
def extend_word(text: CharSequence, offset: Text.Offset): Text.Offset = |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
223 |
{ |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
224 |
val n = text.length |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
225 |
var i = offset |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
226 |
while (i < n && is_word_char(text.charAt(i))) i += 1 |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
227 |
if (i < n && text.charAt(i) == '>' && read_symbol(text.subSequence(0, i + 1)).isDefined) |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
228 |
i + 1 |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
229 |
else i |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
230 |
} |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
231 |
|
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
232 |
def read_symbol(in: CharSequence): Option[String] = |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
233 |
{ |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
234 |
val reverse_in = new Library.Reverse(in) |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
235 |
parse(reverse_symbol ^^ (_.reverse), reverse_in) match { |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
236 |
case Success(result, _) => Some(result) |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
237 |
case _ => None |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
238 |
} |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
239 |
} |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
240 |
|
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
241 |
def read_word(explicit: Boolean, in: CharSequence): Option[(String, String)] = |
31763 | 242 |
{ |
53322 | 243 |
val parse_word = if (explicit) word else word3 |
37072
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents:
36012
diff
changeset
|
244 |
val reverse_in = new Library.Reverse(in) |
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
245 |
val parser = |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
246 |
(reverse_symbol | reverse_symb | escape) ^^ (x => (x.reverse, "")) | |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
247 |
underscores ~ parse_word ^^ { case x ~ y => (y.reverse, x) } |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
248 |
parse(parser, reverse_in) match { |
31763 | 249 |
case Success(result, _) => Some(result) |
250 |
case _ => None |
|
251 |
} |
|
252 |
} |
|
253 |
} |
|
55666 | 254 |
|
255 |
||
256 |
/* abbreviations */ |
|
257 |
||
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
258 |
private val caret_indicator = '\007' |
55666 | 259 |
private val antiquote = "@{" |
260 |
private val default_abbrs = |
|
261 |
Map("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>") |
|
31763 | 262 |
} |
263 |
||
46712 | 264 |
final class Completion private( |
55984 | 265 |
keywords: Map[String, Boolean] = Map.empty, |
46625 | 266 |
words_lex: Scan.Lexicon = Scan.Lexicon.empty, |
53318 | 267 |
words_map: Multi_Map[String, String] = Multi_Map.empty, |
46625 | 268 |
abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty, |
53318 | 269 |
abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty) |
31763 | 270 |
{ |
55983 | 271 |
/* keywords */ |
31763 | 272 |
|
55986
61b0021ed674
more strict discrimination: symbols vs. keywords could overlap;
wenzelm
parents:
55985
diff
changeset
|
273 |
private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name) |
61b0021ed674
more strict discrimination: symbols vs. keywords could overlap;
wenzelm
parents:
55985
diff
changeset
|
274 |
private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name) |
61b0021ed674
more strict discrimination: symbols vs. keywords could overlap;
wenzelm
parents:
55985
diff
changeset
|
275 |
private def is_keyword_template(name: String): Boolean = is_keyword(name) && keywords(name) |
55984 | 276 |
|
277 |
def + (keyword: String, template: String): Completion = |
|
46624 | 278 |
new Completion( |
55984 | 279 |
keywords + (keyword -> (keyword != template)), |
46624 | 280 |
words_lex + keyword, |
55984 | 281 |
words_map + (keyword -> template), |
46624 | 282 |
abbrevs_lex, |
283 |
abbrevs_map) |
|
31763 | 284 |
|
40533
e38e80686ce5
somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents:
37072
diff
changeset
|
285 |
def + (keyword: String): Completion = this + (keyword, keyword) |
e38e80686ce5
somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents:
37072
diff
changeset
|
286 |
|
55983 | 287 |
|
288 |
/* symbols with abbreviations */ |
|
289 |
||
46624 | 290 |
private def add_symbols(): Completion = |
31763 | 291 |
{ |
292 |
val words = |
|
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
293 |
(for ((x, _) <- Symbol.names.toList) yield (x, x)) ::: |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
294 |
(for ((x, y) <- Symbol.names.toList) yield ("\\" + y, x)) ::: |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
295 |
(for ((x, y) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(y)) yield (y, x)) |
31763 | 296 |
|
55666 | 297 |
val symbol_abbrs = |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
298 |
(for ((x, y) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(y)) |
55666 | 299 |
yield (y, x)).toList |
300 |
||
301 |
val abbrs = |
|
302 |
for ((a, b) <- symbol_abbrs ::: Completion.default_abbrs.toList) |
|
303 |
yield (a.reverse, (a, b)) |
|
31763 | 304 |
|
46624 | 305 |
new Completion( |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
306 |
keywords, |
46624 | 307 |
words_lex ++ words.map(_._1), |
308 |
words_map ++ words, |
|
309 |
abbrevs_lex ++ abbrs.map(_._1), |
|
310 |
abbrevs_map ++ abbrs) |
|
31763 | 311 |
} |
312 |
||
313 |
||
314 |
/* complete */ |
|
315 |
||
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
316 |
def complete( |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
317 |
history: Completion.History, |
55977 | 318 |
do_decode: Boolean, |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
319 |
explicit: Boolean, |
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
320 |
start: Text.Offset, |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
321 |
text: CharSequence, |
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
322 |
caret: Int, |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
323 |
extend_word: Boolean, |
55749 | 324 |
language_context: Completion.Language_Context): Option[Completion.Result] = |
31763 | 325 |
{ |
55977 | 326 |
def decode(s: String): String = if (do_decode) Symbol.decode(s) else s |
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
327 |
val length = text.length |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
328 |
|
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
329 |
val abbrevs_result = |
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
330 |
{ |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
331 |
val reverse_in = new Library.Reverse(text.subSequence(0, caret)) |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
332 |
Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), reverse_in) match { |
55666 | 333 |
case Scan.Parsers.Success(reverse_a, _) => |
334 |
val abbrevs = abbrevs_map.get_list(reverse_a) |
|
335 |
abbrevs match { |
|
336 |
case Nil => None |
|
337 |
case (a, _) :: _ => |
|
338 |
val ok = |
|
55749 | 339 |
if (a == Completion.antiquote) language_context.antiquotes |
340 |
else language_context.symbols || Completion.default_abbrs.isDefinedAt(a) |
|
55993 | 341 |
if (ok) Some(((a, abbrevs), caret)) |
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
342 |
else None |
55666 | 343 |
} |
344 |
case _ => None |
|
345 |
} |
|
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
346 |
} |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
347 |
|
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
348 |
val words_result = |
55982 | 349 |
if (abbrevs_result.isDefined) None |
350 |
else { |
|
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
351 |
val end = |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
352 |
if (extend_word) Completion.Word_Parsers.extend_word(text, caret) |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
353 |
else caret |
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
354 |
val result = |
55992 | 355 |
Completion.Word_Parsers.read_symbol(text.subSequence(0, end)) match { |
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
356 |
case Some(symbol) => Some((symbol, "")) |
55992 | 357 |
case None => |
358 |
val word_context = |
|
359 |
end < length && Completion.Word_Parsers.is_word_char(text.charAt(end)) |
|
360 |
if (word_context) None |
|
361 |
else Completion.Word_Parsers.read_word(explicit, text.subSequence(0, end)) |
|
362 |
} |
|
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
363 |
result.map( |
55992 | 364 |
{ |
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
365 |
case (word, underscores) => |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
366 |
val complete_words = words_lex.completions(word) |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
367 |
val full_word = word + underscores |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
368 |
val completions = |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
369 |
if (complete_words.contains(full_word)) Nil |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
370 |
else |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
371 |
for { |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
372 |
complete_word <- complete_words |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
373 |
ok = |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
374 |
if (is_keyword(complete_word)) language_context.is_outer |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
375 |
else language_context.symbols |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
376 |
if ok |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
377 |
completion <- words_map.get_list(complete_word) |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
378 |
} yield (complete_word, completion) |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
379 |
(((full_word, completions), end)) |
55992 | 380 |
}) |
53275 | 381 |
} |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
382 |
|
55982 | 383 |
(abbrevs_result orElse words_result) match { |
55993 | 384 |
case Some(((original, completions), end)) if !completions.isEmpty => |
55985 | 385 |
val range = Text.Range(- original.length, 0) + end + start |
386 |
val immediate = |
|
387 |
explicit || |
|
388 |
(!Completion.Word_Parsers.is_word(original) && |
|
389 |
Character.codePointCount(original, 0, original.length) > 1) |
|
55993 | 390 |
val unique = completions.length == 1 |
55985 | 391 |
|
392 |
val items = |
|
393 |
for { |
|
55993 | 394 |
(complete_word, name0) <- completions |
395 |
name1 = decode(name0) |
|
55985 | 396 |
if name1 != original |
397 |
(s1, s2) = |
|
398 |
space_explode(Completion.caret_indicator, name1) match { |
|
399 |
case List(s1, s2) => (s1, s2) |
|
400 |
case _ => (name1, "") |
|
401 |
} |
|
402 |
move = - s2.length |
|
403 |
description = |
|
404 |
if (is_symbol(name0)) { |
|
405 |
if (name0 == name1) List(name0) |
|
406 |
else List(name1, "(symbol " + quote(name0) + ")") |
|
407 |
} |
|
55993 | 408 |
else if (is_keyword_template(complete_word)) |
409 |
List(name1, "(template " + quote(complete_word) + ")") |
|
410 |
else if (move != 0) List(name1, "(template)") |
|
411 |
else if (is_keyword(complete_word)) List(name1, "(keyword)") |
|
55985 | 412 |
else List(name1) |
413 |
} |
|
414 |
yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate) |
|
415 |
||
416 |
if (items.isEmpty) None |
|
417 |
else Some(Completion.Result(range, original, unique, items.sorted(history.ordering))) |
|
418 |
||
55992 | 419 |
case _ => None |
31765 | 420 |
} |
31763 | 421 |
} |
422 |
} |