author | wenzelm |
Thu, 12 May 2016 10:57:09 +0200 | |
changeset 63086 | 5c8e6a751adc |
parent 62969 | 9f394a16c557 |
child 63135 | 035785035a1a |
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 |
57589 | 14 |
import scala.util.matching.Regex |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
15 |
import scala.math.Ordering |
31763 | 16 |
|
17 |
||
46624 | 18 |
object Completion |
31763 | 19 |
{ |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
20 |
/** completion result **/ |
53275 | 21 |
|
53296
65c60c782da5
less aggressive immediate completion, based on input and text;
wenzelm
parents:
53295
diff
changeset
|
22 |
sealed case class Item( |
55692
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55687
diff
changeset
|
23 |
range: Text.Range, |
53296
65c60c782da5
less aggressive immediate completion, based on input and text;
wenzelm
parents:
53295
diff
changeset
|
24 |
original: String, |
55666 | 25 |
name: String, |
55978 | 26 |
description: List[String], |
53296
65c60c782da5
less aggressive immediate completion, based on input and text;
wenzelm
parents:
53295
diff
changeset
|
27 |
replacement: String, |
55666 | 28 |
move: Int, |
53296
65c60c782da5
less aggressive immediate completion, based on input and text;
wenzelm
parents:
53295
diff
changeset
|
29 |
immediate: Boolean) |
53275 | 30 |
|
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55813
diff
changeset
|
31 |
object Result |
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 |
def empty(range: Text.Range): Result = Result(range, "", false, Nil) |
56175 | 34 |
def merge(history: History, result1: Option[Result], result2: Option[Result]): Option[Result] = |
35 |
(result1, result2) match { |
|
36 |
case (_, None) => result1 |
|
37 |
case (None, _) => result2 |
|
38 |
case (Some(res1), Some(res2)) => |
|
39 |
if (res1.range != res2.range || res1.original != res2.original) result1 |
|
40 |
else { |
|
41 |
val items = (res1.items ::: res2.items).sorted(history.ordering) |
|
42 |
Some(Result(res1.range, res1.original, false, items)) |
|
43 |
} |
|
44 |
} |
|
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55813
diff
changeset
|
45 |
} |
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55813
diff
changeset
|
46 |
|
55693
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
47 |
sealed case class Result( |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
48 |
range: Text.Range, |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
49 |
original: String, |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
50 |
unique: Boolean, |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
51 |
items: List[Item]) |
53325
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53324
diff
changeset
|
52 |
|
53275 | 53 |
|
46624 | 54 |
|
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
55 |
/** persistent history **/ |
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 |
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
|
58 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
59 |
object History |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
60 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
61 |
val empty: History = new 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 |
def load(): History = |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
64 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
65 |
def ignore_error(msg: String): Unit = |
56782
433cf57550fa
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
56661
diff
changeset
|
66 |
Output.warning("Ignoring bad content of file " + COMPLETION_HISTORY + |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
67 |
(if (msg == "") "" else "\n" + msg)) |
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 |
val content = |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
70 |
if (COMPLETION_HISTORY.is_file) { |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
71 |
try { |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
72 |
import XML.Decode._ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
73 |
list(pair(Symbol.decode_string, int))( |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
74 |
YXML.parse_body(File.read(COMPLETION_HISTORY))) |
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 |
catch { |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
77 |
case ERROR(msg) => ignore_error(msg); Nil |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
78 |
case _: XML.Error => ignore_error(""); Nil |
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 |
else Nil |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
82 |
(empty /: content)(_ + _) |
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 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
86 |
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
|
87 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
88 |
override def toString: String = rep.mkString("Completion.History(", ",", ")") |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
89 |
|
56878
a5d082a85124
hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents:
56800
diff
changeset
|
90 |
def frequency(name: String): Int = |
a5d082a85124
hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents:
56800
diff
changeset
|
91 |
default_frequency(Symbol.encode(name)) getOrElse |
a5d082a85124
hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents:
56800
diff
changeset
|
92 |
rep.getOrElse(name, 0) |
53337
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 |
def + (entry: (String, Int)): History = |
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 |
val (name, freq) = entry |
56564
94c55cc73747
added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents:
56278
diff
changeset
|
97 |
if (name == "") this |
94c55cc73747
added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents:
56278
diff
changeset
|
98 |
else new History(rep + (name -> (frequency(name) + freq))) |
53337
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 |
def ordering: Ordering[Item] = |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
102 |
new Ordering[Item] { |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
103 |
def compare(item1: Item, item2: Item): Int = |
56162
ea6303e2261b
clarified completion ordering: prefer local names;
wenzelm
parents:
56042
diff
changeset
|
104 |
frequency(item2.name) compare frequency(item1.name) |
ea6303e2261b
clarified completion ordering: prefer local names;
wenzelm
parents:
56042
diff
changeset
|
105 |
} |
ea6303e2261b
clarified completion ordering: prefer local names;
wenzelm
parents:
56042
diff
changeset
|
106 |
|
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
107 |
def save() |
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 |
Isabelle_System.mkdirs(COMPLETION_HISTORY.dir) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
110 |
File.write_backup(COMPLETION_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 |
import XML.Encode._ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
113 |
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
|
114 |
}) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
115 |
} |
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 |
class History_Variable |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
119 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
120 |
private var history = History.empty |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
121 |
def value: History = synchronized { history } |
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 |
def load() |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
124 |
{ |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
125 |
val h = History.load() |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
126 |
synchronized { history = h } |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
127 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
128 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
129 |
def update(item: Item, freq: Int = 1): Unit = synchronized { |
55666 | 130 |
history = history + (item.name -> freq) |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
131 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
132 |
} |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
133 |
|
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
134 |
|
55694
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 |
/** semantic completion **/ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
137 |
|
61100 | 138 |
def clean_name(s: String): Option[String] = |
139 |
if (s == "" || s == "_") None |
|
140 |
else Some(s.reverseIterator.dropWhile(_ == '_').toList.reverse.mkString) |
|
141 |
||
59717
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
142 |
def report_no_completion(pos: Position.T): String = |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
143 |
YXML.string_of_tree(Semantic.Info(pos, No_Completion)) |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
144 |
|
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
145 |
def report_names(pos: Position.T, total: Int, names: List[(String, (String, String))]): String = |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
146 |
YXML.string_of_tree(Semantic.Info(pos, Names(total, names))) |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
147 |
|
56173 | 148 |
object Semantic |
55694
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 |
object Info |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
151 |
{ |
59717
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
152 |
def apply(pos: Position.T, semantic: Semantic): XML.Elem = |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
153 |
{ |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
154 |
val elem = |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
155 |
semantic match { |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
156 |
case No_Completion => XML.Elem(Markup(Markup.NO_COMPLETION, pos), Nil) |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
157 |
case Names(total, names) => |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
158 |
XML.Elem(Markup(Markup.COMPLETION, pos), |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
159 |
{ |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
160 |
import XML.Encode._ |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
161 |
pair(int, list(pair(string, pair(string, string))))(total, names) |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
162 |
}) |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
163 |
} |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
164 |
XML.Elem(Markup(Markup.REPORT, pos), List(elem)) |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
165 |
} |
44a3ed0b8265
support for completion reports produced in Scala (inlined into messages);
wenzelm
parents:
59319
diff
changeset
|
166 |
|
56173 | 167 |
def unapply(info: Text.Markup): Option[Text.Info[Semantic]] = |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
168 |
info.info match { |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
169 |
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
|
170 |
try { |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
171 |
val (total, names) = |
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 |
import XML.Decode._ |
55977 | 174 |
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
|
175 |
} |
56173 | 176 |
Some(Text.Info(info.range, Names(total, names))) |
55694
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 |
catch { case _: XML.Error => None } |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55813
diff
changeset
|
179 |
case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) => |
56173 | 180 |
Some(Text.Info(info.range, No_Completion)) |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
181 |
case _ => None |
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 |
} |
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 |
|
56173 | 186 |
sealed abstract class Semantic |
56175 | 187 |
case object No_Completion extends Semantic |
188 |
case class Names(total: Int, names: List[(String, (String, String))]) extends Semantic |
|
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 |
def complete( |
56173 | 191 |
range: Text.Range, |
192 |
history: Completion.History, |
|
193 |
do_decode: Boolean, |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
194 |
original: String): Option[Completion.Result] = |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
195 |
{ |
55977 | 196 |
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
|
197 |
val items = |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
198 |
for { |
55977 | 199 |
(xname, (kind, name)) <- names |
200 |
xname1 = decode(xname) |
|
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
201 |
if xname1 != original |
55977 | 202 |
(full_name, descr_name) = |
203 |
if (kind == "") (name, quote(decode(name))) |
|
56600 | 204 |
else |
56800 | 205 |
(Long_Name.qualify(kind, name), |
60732 | 206 |
Word.implode(Word.explode('_', kind)) + |
207 |
(if (xname == name) "" else " " + quote(decode(name)))) |
|
61622
8bb7848b3d47
smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents:
61613
diff
changeset
|
208 |
} yield { |
8bb7848b3d47
smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents:
61613
diff
changeset
|
209 |
val description = List(xname1, "(" + descr_name + ")") |
8bb7848b3d47
smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents:
61613
diff
changeset
|
210 |
val replacement = |
8bb7848b3d47
smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents:
61613
diff
changeset
|
211 |
Token.explode(Keyword.Keywords.empty, xname1) match { |
62969 | 212 |
case List(tok) if tok.is_name => xname1 |
61622
8bb7848b3d47
smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents:
61613
diff
changeset
|
213 |
case _ => quote(xname1) |
8bb7848b3d47
smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents:
61613
diff
changeset
|
214 |
} |
8bb7848b3d47
smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents:
61613
diff
changeset
|
215 |
Item(range, original, full_name, description, replacement, 0, true) |
8bb7848b3d47
smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents:
61613
diff
changeset
|
216 |
} |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
217 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
218 |
if (items.isEmpty) None |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
219 |
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
|
220 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
221 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
222 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
223 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
224 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
225 |
/** syntactic completion **/ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
226 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
227 |
/* language context */ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
228 |
|
55749 | 229 |
object Language_Context |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
230 |
{ |
55749 | 231 |
val outer = Language_Context("", true, false) |
232 |
val inner = Language_Context(Markup.Language.UNKNOWN, true, false) |
|
233 |
val ML_outer = Language_Context(Markup.Language.ML, false, true) |
|
234 |
val ML_inner = Language_Context(Markup.Language.ML, true, false) |
|
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56221
diff
changeset
|
235 |
val SML_outer = Language_Context(Markup.Language.SML, false, false) |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
236 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
237 |
|
55749 | 238 |
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
|
239 |
{ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
240 |
def is_outer: Boolean = language == "" |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
241 |
} |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
242 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
243 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
244 |
/* init */ |
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
245 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
246 |
val empty: Completion = new Completion() |
61960 | 247 |
def init(): Completion = empty.load() |
55694
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
248 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
249 |
|
a1184dfb8e00
clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents:
55693
diff
changeset
|
250 |
/* word parsers */ |
31763 | 251 |
|
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
252 |
private object Word_Parsers extends RegexParsers |
31763 | 253 |
{ |
254 |
override val whiteSpace = "".r |
|
255 |
||
61613 | 256 |
private val symboloid_regex: Regex = """\\([A-Za-z0-9_']+|<\^?[A-Za-z0-9_']+>?)""".r |
61600
1ca11ddfcc70
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
wenzelm
parents:
61599
diff
changeset
|
257 |
def is_symboloid(s: CharSequence): Boolean = symboloid_regex.pattern.matcher(s).matches |
57589 | 258 |
|
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
259 |
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
|
260 |
private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r |
61599 | 261 |
private def reverse_escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
262 |
|
56039
5ff5208de089
include long identifiers in the reckoning of words (e.g. "integer.lifting" vs. 'lifting_update');
wenzelm
parents:
56001
diff
changeset
|
263 |
private val word_regex = "[a-zA-Z0-9_'.]+".r |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
264 |
private def word: Parser[String] = word_regex |
56039
5ff5208de089
include long identifiers in the reckoning of words (e.g. "integer.lifting" vs. 'lifting_update');
wenzelm
parents:
56001
diff
changeset
|
265 |
private def word3: Parser[String] = "[a-zA-Z0-9_'.]{3,}".r |
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
266 |
private def underscores: Parser[String] = "_*".r |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
267 |
|
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
268 |
def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches |
56042
d3c35a300433
proper Char comparison, despite weakly-typed Scala (cf. 5ff5208de089);
wenzelm
parents:
56039
diff
changeset
|
269 |
def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.' |
31763 | 270 |
|
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
271 |
def read_symbol(in: CharSequence): Option[String] = |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
272 |
{ |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
273 |
val reverse_in = new Library.Reverse(in) |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
274 |
parse(reverse_symbol ^^ (_.reverse), reverse_in) match { |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
275 |
case Success(result, _) => Some(result) |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
276 |
case _ => None |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
277 |
} |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
278 |
} |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
279 |
|
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
280 |
def read_word(explicit: Boolean, in: CharSequence): Option[(String, String)] = |
31763 | 281 |
{ |
53322 | 282 |
val parse_word = if (explicit) word else word3 |
37072
9105c8237c7a
renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents:
36012
diff
changeset
|
283 |
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
|
284 |
val parser = |
61599 | 285 |
(reverse_symbol | reverse_symb | reverse_escape) ^^ (x => (x.reverse, "")) | |
56221
a8dfbe9f25da
accomodate word as part of schematic variable name;
wenzelm
parents:
56175
diff
changeset
|
286 |
underscores ~ parse_word ~ opt("?") ^^ |
a8dfbe9f25da
accomodate word as part of schematic variable name;
wenzelm
parents:
56175
diff
changeset
|
287 |
{ case x ~ y ~ z => (z.getOrElse("") + y.reverse, x) } |
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
288 |
parse(parser, reverse_in) match { |
31763 | 289 |
case Success(result, _) => Some(result) |
290 |
case _ => None |
|
291 |
} |
|
292 |
} |
|
293 |
} |
|
55666 | 294 |
|
295 |
||
296 |
/* abbreviations */ |
|
297 |
||
61960 | 298 |
private object Abbrevs_Parser extends Parse.Parser |
299 |
{ |
|
300 |
private val syntax = Outer_Syntax.empty + "=" |
|
301 |
||
302 |
private val entry: Parser[(String, String)] = |
|
303 |
text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) } |
|
304 |
||
305 |
def parse_file(file: Path): List[(String, String)] = |
|
306 |
{ |
|
307 |
val toks = Token.explode(syntax.keywords, File.read(file)) |
|
308 |
parse_all(rep(entry), Token.reader(toks, Token.Pos.file(file.implode))) match { |
|
309 |
case Success(result, _) => result |
|
310 |
case bad => error(bad.toString) |
|
311 |
} |
|
312 |
} |
|
313 |
} |
|
314 |
||
315 |
def load_abbrevs(): List[(String, String)] = |
|
316 |
{ |
|
317 |
val symbol_abbrevs = |
|
318 |
for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym) |
|
319 |
val more_abbrevs = |
|
320 |
for { |
|
321 |
path <- Path.split(Isabelle_System.getenv("ISABELLE_ABBREVS")) |
|
322 |
if path.is_file |
|
323 |
entry <- Abbrevs_Parser.parse_file(path) |
|
324 |
} yield entry |
|
62232 | 325 |
val remove_abbrevs = (for { (a, b) <- more_abbrevs if b == "" } yield a).toSet |
326 |
||
327 |
(symbol_abbrevs ::: more_abbrevs).filterNot({ case (a, _) => remove_abbrevs.contains(a) }) |
|
61960 | 328 |
} |
329 |
||
56661
ef623f6f036b
avoid octal escape literals -- deprecated in scala-2.11.0;
wenzelm
parents:
56600
diff
changeset
|
330 |
private val caret_indicator = '\u0007' |
55666 | 331 |
private val antiquote = "@{" |
56878
a5d082a85124
hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents:
56800
diff
changeset
|
332 |
|
55666 | 333 |
private val default_abbrs = |
56878
a5d082a85124
hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents:
56800
diff
changeset
|
334 |
List("@{" -> "@{\u0007}", |
a5d082a85124
hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents:
56800
diff
changeset
|
335 |
"`" -> "\\<close>", |
a5d082a85124
hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents:
56800
diff
changeset
|
336 |
"`" -> "\\<open>", |
a5d082a85124
hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents:
56800
diff
changeset
|
337 |
"`" -> "\\<open>\u0007\\<close>") |
a5d082a85124
hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents:
56800
diff
changeset
|
338 |
|
a5d082a85124
hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents:
56800
diff
changeset
|
339 |
private def default_frequency(name: String): Option[Int] = |
a5d082a85124
hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents:
56800
diff
changeset
|
340 |
default_abbrs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2) |
31763 | 341 |
} |
342 |
||
46712 | 343 |
final class Completion private( |
59073 | 344 |
protected val keywords: Map[String, Boolean] = Map.empty, |
345 |
protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty, |
|
346 |
protected val words_map: Multi_Map[String, String] = Multi_Map.empty, |
|
347 |
protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty, |
|
348 |
protected val abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty) |
|
31763 | 349 |
{ |
59073 | 350 |
/* merge */ |
351 |
||
352 |
def is_empty: Boolean = |
|
353 |
keywords.isEmpty && |
|
354 |
words_lex.is_empty && |
|
355 |
words_map.isEmpty && |
|
356 |
abbrevs_lex.is_empty && |
|
357 |
abbrevs_map.isEmpty |
|
358 |
||
359 |
def ++ (other: Completion): Completion = |
|
360 |
if (this eq other) this |
|
361 |
else if (is_empty) other |
|
362 |
else { |
|
363 |
val keywords1 = |
|
364 |
(keywords /: other.keywords) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e } |
|
365 |
val words_lex1 = words_lex ++ other.words_lex |
|
366 |
val words_map1 = words_map ++ other.words_map |
|
367 |
val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex |
|
368 |
val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map |
|
369 |
new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1) |
|
370 |
} |
|
371 |
||
372 |
||
55983 | 373 |
/* keywords */ |
31763 | 374 |
|
55986
61b0021ed674
more strict discrimination: symbols vs. keywords could overlap;
wenzelm
parents:
55985
diff
changeset
|
375 |
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
|
376 |
private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name) |
56001
2df1e7bca361
do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);
wenzelm
parents:
55996
diff
changeset
|
377 |
private def is_keyword_template(name: String, template: Boolean): Boolean = |
2df1e7bca361
do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);
wenzelm
parents:
55996
diff
changeset
|
378 |
is_keyword(name) && keywords(name) == template |
55984 | 379 |
|
380 |
def + (keyword: String, template: String): Completion = |
|
46624 | 381 |
new Completion( |
55984 | 382 |
keywords + (keyword -> (keyword != template)), |
46624 | 383 |
words_lex + keyword, |
55984 | 384 |
words_map + (keyword -> template), |
46624 | 385 |
abbrevs_lex, |
386 |
abbrevs_map) |
|
31763 | 387 |
|
40533
e38e80686ce5
somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents:
37072
diff
changeset
|
388 |
def + (keyword: String): Completion = this + (keyword, keyword) |
e38e80686ce5
somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents:
37072
diff
changeset
|
389 |
|
55983 | 390 |
|
61960 | 391 |
/* load symbols and abbrevs */ |
55983 | 392 |
|
61960 | 393 |
private def load(): Completion = |
31763 | 394 |
{ |
61960 | 395 |
val abbrevs = Completion.load_abbrevs() |
396 |
||
31763 | 397 |
val words = |
61599 | 398 |
(for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) ::: |
399 |
(for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym)) ::: |
|
61960 | 400 |
(for ((abbr, text) <- abbrevs if Completion.Word_Parsers.is_word(abbr)) yield (abbr, text)) |
31763 | 401 |
|
61960 | 402 |
val non_word_abbrs = |
403 |
(for ((abbr, text) <- abbrevs if !Completion.Word_Parsers.is_word(abbr)) |
|
404 |
yield (abbr, text)).toList |
|
55666 | 405 |
|
406 |
val abbrs = |
|
61960 | 407 |
for ((abbr, text) <- non_word_abbrs ::: Completion.default_abbrs) |
408 |
yield (abbr.reverse, (abbr, text)) |
|
31763 | 409 |
|
46624 | 410 |
new Completion( |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
411 |
keywords, |
46624 | 412 |
words_lex ++ words.map(_._1), |
413 |
words_map ++ words, |
|
414 |
abbrevs_lex ++ abbrs.map(_._1), |
|
415 |
abbrevs_map ++ abbrs) |
|
31763 | 416 |
} |
417 |
||
418 |
||
419 |
/* complete */ |
|
420 |
||
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
421 |
def complete( |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
422 |
history: Completion.History, |
55977 | 423 |
do_decode: Boolean, |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
424 |
explicit: Boolean, |
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
425 |
start: Text.Offset, |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
426 |
text: CharSequence, |
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
427 |
caret: Int, |
55749 | 428 |
language_context: Completion.Language_Context): Option[Completion.Result] = |
31763 | 429 |
{ |
55977 | 430 |
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
|
431 |
val length = text.length |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
432 |
|
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
433 |
val abbrevs_result = |
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
434 |
{ |
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
435 |
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
|
436 |
Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), reverse_in) match { |
61599 | 437 |
case Scan.Parsers.Success(reverse_abbr, _) => |
438 |
val abbrevs = abbrevs_map.get_list(reverse_abbr) |
|
55666 | 439 |
abbrevs match { |
440 |
case Nil => None |
|
61599 | 441 |
case (abbr, _) :: _ => |
55666 | 442 |
val ok = |
61599 | 443 |
if (abbr == Completion.antiquote) language_context.antiquotes |
61600
1ca11ddfcc70
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
wenzelm
parents:
61599
diff
changeset
|
444 |
else language_context.symbols || Completion.default_abbrs.exists(_._1 == abbr) |
61599 | 445 |
if (ok) Some((abbr, abbrevs)) |
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
446 |
else None |
55666 | 447 |
} |
448 |
case _ => None |
|
449 |
} |
|
55813
08a1c860bc12
allow completion within a word (or symbol), like semantic completion;
wenzelm
parents:
55749
diff
changeset
|
450 |
} |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
451 |
|
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
452 |
val words_result = |
55982 | 453 |
if (abbrevs_result.isDefined) None |
454 |
else { |
|
57602
0f708666eb7c
no keyword completion within word context -- especially avoid its odd visual rendering;
wenzelm
parents:
57589
diff
changeset
|
455 |
val word_context = |
0f708666eb7c
no keyword completion within word context -- especially avoid its odd visual rendering;
wenzelm
parents:
57589
diff
changeset
|
456 |
caret < length && Completion.Word_Parsers.is_word_char(text.charAt(caret)) |
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
457 |
val result = |
57588
ff31aad27661
discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
wenzelm
parents:
56878
diff
changeset
|
458 |
Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match { |
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
459 |
case Some(symbol) => Some((symbol, "")) |
57588
ff31aad27661
discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
wenzelm
parents:
56878
diff
changeset
|
460 |
case None => Completion.Word_Parsers.read_word(explicit, text.subSequence(0, caret)) |
55992 | 461 |
} |
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
462 |
result.map( |
55992 | 463 |
{ |
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
464 |
case (word, underscores) => |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
465 |
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
|
466 |
val full_word = word + underscores |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
467 |
val completions = |
56001
2df1e7bca361
do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);
wenzelm
parents:
55996
diff
changeset
|
468 |
if (complete_words.contains(full_word) && is_keyword_template(full_word, false)) Nil |
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
469 |
else |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
470 |
for { |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
471 |
complete_word <- complete_words |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
472 |
ok = |
57602
0f708666eb7c
no keyword completion within word context -- especially avoid its odd visual rendering;
wenzelm
parents:
57589
diff
changeset
|
473 |
if (is_keyword(complete_word)) !word_context && language_context.is_outer |
61600
1ca11ddfcc70
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
wenzelm
parents:
61599
diff
changeset
|
474 |
else language_context.symbols || Completion.Word_Parsers.is_symboloid(word) |
55996
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
475 |
if ok |
13a7d9661ffc
allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents:
55994
diff
changeset
|
476 |
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
|
477 |
} yield (complete_word, completion) |
60215 | 478 |
(full_word, completions) |
55992 | 479 |
}) |
53275 | 480 |
} |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55497
diff
changeset
|
481 |
|
55982 | 482 |
(abbrevs_result orElse words_result) match { |
59319 | 483 |
case Some((original, completions)) if completions.nonEmpty => |
57588
ff31aad27661
discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
wenzelm
parents:
56878
diff
changeset
|
484 |
val range = Text.Range(- original.length, 0) + caret + start |
55985 | 485 |
val immediate = |
486 |
explicit || |
|
487 |
(!Completion.Word_Parsers.is_word(original) && |
|
61600
1ca11ddfcc70
clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
wenzelm
parents:
61599
diff
changeset
|
488 |
!Completion.Word_Parsers.is_symboloid(original) && |
55985 | 489 |
Character.codePointCount(original, 0, original.length) > 1) |
55993 | 490 |
val unique = completions.length == 1 |
55985 | 491 |
|
492 |
val items = |
|
493 |
for { |
|
55993 | 494 |
(complete_word, name0) <- completions |
495 |
name1 = decode(name0) |
|
55985 | 496 |
if name1 != original |
497 |
(s1, s2) = |
|
498 |
space_explode(Completion.caret_indicator, name1) match { |
|
499 |
case List(s1, s2) => (s1, s2) |
|
500 |
case _ => (name1, "") |
|
501 |
} |
|
502 |
move = - s2.length |
|
503 |
description = |
|
504 |
if (is_symbol(name0)) { |
|
505 |
if (name0 == name1) List(name0) |
|
506 |
else List(name1, "(symbol " + quote(name0) + ")") |
|
507 |
} |
|
56001
2df1e7bca361
do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);
wenzelm
parents:
55996
diff
changeset
|
508 |
else if (is_keyword_template(complete_word, true)) |
55993 | 509 |
List(name1, "(template " + quote(complete_word) + ")") |
510 |
else if (move != 0) List(name1, "(template)") |
|
511 |
else if (is_keyword(complete_word)) List(name1, "(keyword)") |
|
55985 | 512 |
else List(name1) |
513 |
} |
|
514 |
yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate) |
|
515 |
||
516 |
if (items.isEmpty) None |
|
56174 | 517 |
else |
518 |
Some(Completion.Result(range, original, unique, |
|
519 |
items.sortBy(_.name).sorted(history.ordering))) |
|
55985 | 520 |
|
55992 | 521 |
case _ => None |
31765 | 522 |
} |
31763 | 523 |
} |
524 |
} |