author | wenzelm |
Tue, 25 Feb 2014 20:46:09 +0100 | |
changeset 55748 | 2e1398b484aa |
parent 55714 | ed1b789d0b21 |
child 55749 | 75a48dc4383e |
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, |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
24 |
description: 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) |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
28 |
{ override def toString: String = description } |
53275 | 29 |
|
55693
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
30 |
sealed case class Result( |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
31 |
range: Text.Range, |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
32 |
original: String, |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
33 |
unique: Boolean, |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
34 |
items: List[Item]) |
53325
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53324
diff
changeset
|
35 |
|
53275 | 36 |
|
46624 | 37 |
|
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
38 |
/** persistent history **/ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
39 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
40 |
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
|
41 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
42 |
object 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 |
val empty: History = new 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 |
def load(): 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 |
def ignore_error(msg: String): Unit = |
55618 | 49 |
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
|
50 |
(if (msg == "") "" else "\n" + msg)) |
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 |
val content = |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
53 |
if (COMPLETION_HISTORY.is_file) { |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
54 |
try { |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
55 |
import XML.Decode._ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
56 |
list(pair(Symbol.decode_string, int))( |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
57 |
YXML.parse_body(File.read(COMPLETION_HISTORY))) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
58 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
59 |
catch { |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
60 |
case ERROR(msg) => ignore_error(msg); Nil |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
61 |
case _: XML.Error => ignore_error(""); Nil |
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 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
64 |
else Nil |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
65 |
(empty /: content)(_ + _) |
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 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
69 |
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
|
70 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
71 |
override def toString: String = rep.mkString("Completion.History(", ",", ")") |
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 |
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
|
74 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
75 |
def + (entry: (String, Int)): 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 |
val (name, freq) = entry |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
78 |
new History(rep + (name -> (frequency(name) + freq))) |
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 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
81 |
def ordering: Ordering[Item] = |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
82 |
new Ordering[Item] { |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
83 |
def compare(item1: Item, item2: Item): Int = |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
84 |
{ |
55666 | 85 |
frequency(item1.name) compare frequency(item2.name) match { |
86 |
case 0 => item1.name compare item2.name |
|
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
87 |
case ord => - ord |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
88 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
89 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
90 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
91 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
92 |
def save() |
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 |
Isabelle_System.mkdirs(COMPLETION_HISTORY.dir) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
95 |
File.write_backup(COMPLETION_HISTORY, |
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 |
import XML.Encode._ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
98 |
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
|
99 |
}) |
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 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
102 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
103 |
class History_Variable |
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 |
private var history = History.empty |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
106 |
def value: History = synchronized { history } |
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 |
def load() |
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 |
val h = History.load() |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
111 |
synchronized { history = h } |
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 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
114 |
def update(item: Item, freq: Int = 1): Unit = synchronized { |
55666 | 115 |
history = history + (item.name -> freq) |
53337
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 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
119 |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
120 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
121 |
/** semantic completion **/ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
122 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
123 |
object Names |
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 |
object Info |
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 |
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
|
128 |
info.info match { |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
129 |
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
|
130 |
try { |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
131 |
val (total, names) = |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
132 |
{ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
133 |
import XML.Decode._ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
134 |
pair(int, list(pair(string, string)))(body) |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
135 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
136 |
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
|
137 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
138 |
catch { case _: XML.Error => None } |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
139 |
case _ => None |
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 |
} |
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 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
144 |
sealed case class Names(range: Text.Range, total: Int, names: List[(String, String)]) |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
145 |
{ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
146 |
def complete( |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
147 |
history: Completion.History, |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
148 |
decode: Boolean, |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
149 |
original: String): Option[Completion.Result] = |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
150 |
{ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
151 |
val items = |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
152 |
for { |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
153 |
(xname, name) <- names |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
154 |
xname1 = (if (decode) Symbol.decode(xname) else xname) |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
155 |
if xname1 != original |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
156 |
} yield Item(range, original, name, xname1, xname1, 0, true) |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
157 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
158 |
if (items.isEmpty) None |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
159 |
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
|
160 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
161 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
162 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
163 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
164 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
165 |
/** syntactic completion **/ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
166 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
167 |
/* language context */ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
168 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
169 |
object Context |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
170 |
{ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
171 |
val outer = Context("", true, false) |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
172 |
val inner = Context(Markup.Language.UNKNOWN, true, false) |
55714 | 173 |
val ML_outer = Context(Markup.Language.ML, false, true) |
174 |
val ML_inner = 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
|
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 |
sealed case class Context(language: String, symbols: Boolean, antiquotes: Boolean) |
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 |
def is_outer: Boolean = language == "" |
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 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
182 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
183 |
/* init */ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
184 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
185 |
val empty: Completion = new Completion() |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
186 |
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
|
187 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
188 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
189 |
/* word parsers */ |
31763 | 190 |
|
55748 | 191 |
def word_context(text: Option[String]): Boolean = |
192 |
text match { |
|
193 |
case None => false |
|
194 |
case Some(s) => Word_Parsers.is_word(s) |
|
195 |
} |
|
196 |
||
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
197 |
private object Word_Parsers extends RegexParsers |
31763 | 198 |
{ |
199 |
override val whiteSpace = "".r |
|
200 |
||
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
201 |
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
|
202 |
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
|
203 |
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
|
204 |
|
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
205 |
private val word_regex = "[a-zA-Z0-9_']+".r |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
206 |
private def word: Parser[String] = word_regex |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
207 |
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
|
208 |
|
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
209 |
def is_word(s: CharSequence): Boolean = |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
210 |
word_regex.pattern.matcher(s).matches |
31763 | 211 |
|
53322 | 212 |
def read(explicit: Boolean, in: CharSequence): Option[String] = |
31763 | 213 |
{ |
53322 | 214 |
val parse_word = if (explicit) word else word3 |
37072
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents:
36012
diff
changeset
|
215 |
val reverse_in = new Library.Reverse(in) |
53322 | 216 |
parse((reverse_symbol | reverse_symb | escape | parse_word) ^^ (_.reverse), reverse_in) match { |
31763 | 217 |
case Success(result, _) => Some(result) |
218 |
case _ => None |
|
219 |
} |
|
220 |
} |
|
221 |
} |
|
55666 | 222 |
|
223 |
||
224 |
/* abbreviations */ |
|
225 |
||
226 |
private val caret = '\007' |
|
227 |
private val antiquote = "@{" |
|
228 |
private val default_abbrs = |
|
229 |
Map("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>") |
|
31763 | 230 |
} |
231 |
||
46712 | 232 |
final class Completion private( |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
233 |
keywords: Set[String] = Set.empty, |
46625 | 234 |
words_lex: Scan.Lexicon = Scan.Lexicon.empty, |
53318 | 235 |
words_map: Multi_Map[String, String] = Multi_Map.empty, |
46625 | 236 |
abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty, |
53318 | 237 |
abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty) |
31763 | 238 |
{ |
239 |
/* adding stuff */ |
|
240 |
||
40533
e38e80686ce5
somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents:
37072
diff
changeset
|
241 |
def + (keyword: String, replace: String): Completion = |
46624 | 242 |
new Completion( |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
243 |
keywords + keyword, |
46624 | 244 |
words_lex + keyword, |
245 |
words_map + (keyword -> replace), |
|
246 |
abbrevs_lex, |
|
247 |
abbrevs_map) |
|
31763 | 248 |
|
40533
e38e80686ce5
somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents:
37072
diff
changeset
|
249 |
def + (keyword: String): Completion = this + (keyword, keyword) |
e38e80686ce5
somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents:
37072
diff
changeset
|
250 |
|
46624 | 251 |
private def add_symbols(): Completion = |
31763 | 252 |
{ |
253 |
val words = |
|
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
254 |
(for ((x, _) <- Symbol.names.toList) yield (x, x)) ::: |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
255 |
(for ((x, y) <- Symbol.names.toList) yield ("\\" + y, x)) ::: |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
256 |
(for ((x, y) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(y)) yield (y, x)) |
31763 | 257 |
|
55666 | 258 |
val symbol_abbrs = |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
259 |
(for ((x, y) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(y)) |
55666 | 260 |
yield (y, x)).toList |
261 |
||
262 |
val abbrs = |
|
263 |
for ((a, b) <- symbol_abbrs ::: Completion.default_abbrs.toList) |
|
264 |
yield (a.reverse, (a, b)) |
|
31763 | 265 |
|
46624 | 266 |
new Completion( |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
267 |
keywords, |
46624 | 268 |
words_lex ++ words.map(_._1), |
269 |
words_map ++ words, |
|
270 |
abbrevs_lex ++ abbrs.map(_._1), |
|
271 |
abbrevs_map ++ abbrs) |
|
31763 | 272 |
} |
273 |
||
274 |
||
275 |
/* complete */ |
|
276 |
||
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
277 |
def complete( |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
278 |
history: Completion.History, |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
279 |
decode: Boolean, |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
280 |
explicit: Boolean, |
55692
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55687
diff
changeset
|
281 |
text_start: Text.Offset, |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
282 |
text: CharSequence, |
55748 | 283 |
word_context: Boolean, |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
284 |
context: Completion.Context): Option[Completion.Result] = |
31763 | 285 |
{ |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
286 |
val abbrevs_result = |
55666 | 287 |
Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(text)) match { |
288 |
case Scan.Parsers.Success(reverse_a, _) => |
|
289 |
val abbrevs = abbrevs_map.get_list(reverse_a) |
|
290 |
abbrevs match { |
|
291 |
case Nil => None |
|
292 |
case (a, _) :: _ => |
|
293 |
val ok = |
|
294 |
if (a == Completion.antiquote) context.antiquotes |
|
295 |
else context.symbols || Completion.default_abbrs.isDefinedAt(a) |
|
296 |
if (ok) Some((a, abbrevs.map(_._2))) else None |
|
297 |
} |
|
298 |
case _ => None |
|
299 |
} |
|
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
300 |
|
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
301 |
val words_result = |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
302 |
abbrevs_result orElse { |
55748 | 303 |
if (word_context) None |
304 |
else |
|
305 |
Completion.Word_Parsers.read(explicit, text) match { |
|
306 |
case Some(word) => |
|
307 |
val completions = |
|
308 |
for { |
|
309 |
s <- words_lex.completions(word) |
|
310 |
if (if (keywords(s)) context.is_outer else context.symbols) |
|
311 |
r <- words_map.get_list(s) |
|
312 |
} yield r |
|
313 |
if (completions.isEmpty) None |
|
314 |
else Some(word, completions) |
|
315 |
case None => None |
|
316 |
} |
|
53275 | 317 |
} |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
318 |
|
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
319 |
words_result match { |
53275 | 320 |
case Some((word, cs)) => |
55693
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
321 |
val range = Text.Range(- word.length, 0) + (text_start + text.length) |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
322 |
val ds = (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word) |
53275 | 323 |
if (ds.isEmpty) None |
53296
65c60c782da5
less aggressive immediate completion, based on input and text;
wenzelm
parents:
53295
diff
changeset
|
324 |
else { |
53313 | 325 |
val immediate = |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
326 |
!Completion.Word_Parsers.is_word(word) && |
53313 | 327 |
Character.codePointCount(word, 0, word.length) > 1 |
55666 | 328 |
val items = |
329 |
ds.map(s => { |
|
330 |
val (s1, s2) = |
|
331 |
space_explode(Completion.caret, s) match { |
|
332 |
case List(s1, s2) => (s1, s2) |
|
333 |
case _ => (s, "") |
|
334 |
} |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
335 |
Completion.Item(range, word, s, s, s1 + s2, - s2.length, explicit || immediate) |
55666 | 336 |
}) |
55693
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
337 |
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
|
338 |
} |
53275 | 339 |
case None => None |
31765 | 340 |
} |
31763 | 341 |
} |
342 |
} |