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