--- a/src/Pure/PIDE/rendering.scala Mon Jun 19 19:59:13 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala Mon Jun 19 20:32:06 2017 +0200
@@ -212,6 +212,15 @@
def model: Document.Model
+ /* caret */
+
+ def before_caret_range(caret: Text.Offset): Text.Range =
+ {
+ val former_caret = snapshot.revert(caret)
+ snapshot.convert(Text.Range(former_caret - 1, former_caret))
+ }
+
+
/* completion */
def semantic_completion(completed_range: Option[Text.Range], caret_range: Text.Range)
--- a/src/Pure/Tools/spell_checker.scala Mon Jun 19 19:59:13 2017 +0200
+++ b/src/Pure/Tools/spell_checker.scala Mon Jun 19 20:32:06 2017 +0200
@@ -219,7 +219,7 @@
Spell_Checker.marked_words(base, text, info => !check(info.info))
- /* suggestions for unknown words */
+ /* completion: suggestions for unknown words */
private def suggestions(word: String): Option[List[String]] =
{
@@ -249,6 +249,19 @@
}
def complete_enabled(word: String): Boolean = complete(word).nonEmpty
+
+ def completion(rendering: Rendering, caret: Text.Offset): Option[Completion.Result] =
+ {
+ val caret_range = rendering.before_caret_range(caret)
+ for {
+ word <- Spell_Checker.current_word(rendering, caret_range)
+ words = complete(word.info)
+ if words.nonEmpty
+ descr = "(from dictionary " + quote(dictionary.toString) + ")"
+ items =
+ words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
+ } yield Completion.Result(word.range, word.info, false, items)
+ }
}
--- a/src/Tools/VSCode/src/vscode_rendering.scala Mon Jun 19 19:59:13 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Mon Jun 19 20:32:06 2017 +0200
@@ -75,12 +75,6 @@
/* completion */
- def before_caret_range(caret: Text.Offset): Text.Range =
- {
- val former_caret = snapshot.revert(caret)
- snapshot.convert(Text.Range(former_caret - 1, former_caret))
- }
-
def completion(caret_pos: Line.Position, caret: Text.Offset): List[Protocol.CompletionItem] =
{
val doc = model.content.doc
--- a/src/Tools/jEdit/src/bibtex_jedit.scala Mon Jun 19 19:59:13 2017 +0200
+++ b/src/Tools/jEdit/src/bibtex_jedit.scala Mon Jun 19 20:32:06 2017 +0200
@@ -37,11 +37,11 @@
def completion(
history: Completion.History,
- text_area: JEditTextArea,
- rendering: JEdit_Rendering): Option[Completion.Result] =
+ rendering: JEdit_Rendering,
+ caret: Text.Offset): Option[Completion.Result] =
{
for {
- Text.Info(r, name) <- rendering.citation(JEdit_Lib.before_caret_range(text_area, rendering))
+ Text.Info(r, name) <- rendering.citation(rendering.before_caret_range(caret))
name1 <- Completion.clean_name(name)
original <- rendering.model.try_get_text(r)
--- a/src/Tools/jEdit/src/completion_popup.scala Mon Jun 19 19:59:13 2017 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Mon Jun 19 20:32:06 2017 +0200
@@ -125,15 +125,16 @@
active_range match {
case Some(range) => range.try_restrict(line_range)
case None =>
- if (line_range.contains(text_area.getCaretPosition)) {
- JEdit_Lib.before_caret_range(text_area, rendering).try_restrict(line_range) match {
+ val caret = text_area.getCaretPosition
+ if (line_range.contains(caret)) {
+ rendering.before_caret_range(caret).try_restrict(line_range) match {
case Some(range) if !range.is_singularity =>
val range0 =
Completion.Result.merge(Completion.History.empty,
syntax_completion(Completion.History.empty, true, Some(rendering)),
Completion.Result.merge(Completion.History.empty,
path_completion(rendering),
- Bibtex_JEdit.completion(Completion.History.empty, text_area, rendering)))
+ Bibtex_JEdit.completion(Completion.History.empty, rendering, caret)))
.map(_.range)
rendering.semantic_completion(range0, range) match {
case None => range0
@@ -164,7 +165,7 @@
(for {
rendering <- opt_rendering
if PIDE.options.bool("jedit_completion_context")
- caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
+ caret_range = rendering.before_caret_range(text_area.getCaretPosition)
context <- rendering.language_context(caret_range)
} yield context) getOrElse syntax.language_context
@@ -226,7 +227,7 @@
s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded)
for {
- r1 <- rendering.language_path(JEdit_Lib.before_caret_range(text_area, rendering))
+ r1 <- rendering.language_path(rendering.before_caret_range(text_area.getCaretPosition))
s1 <- JEdit_Lib.try_get_text(text_area.getBuffer, r1)
if is_wrapped(s1)
r2 = Text.Range(r1.start + 1, r1.stop - 1)
@@ -349,6 +350,7 @@
}
if (buffer.isEditable) {
+ val caret = text_area.getCaretPosition
val opt_rendering = Document_View.get(text_area).map(_.get_rendering())
val result0 = syntax_completion(history, explicit, opt_rendering)
val (no_completion, semantic_completion) =
@@ -356,7 +358,7 @@
opt_rendering match {
case Some(rendering) =>
rendering.semantic_completion_result(history, unicode, result0.map(_.range),
- JEdit_Lib.before_caret_range(text_area, rendering))
+ rendering.before_caret_range(caret))
case None => (false, None)
}
}
@@ -372,10 +374,10 @@
case Some(rendering) =>
Completion.Result.merge(history, result1,
Completion.Result.merge(history,
- JEdit_Spell_Checker.completion(text_area, explicit, rendering),
+ JEdit_Spell_Checker.completion(rendering, explicit, caret),
Completion.Result.merge(history,
path_completion(rendering),
- Bibtex_JEdit.completion(history, text_area, rendering))))
+ Bibtex_JEdit.completion(history, rendering, caret))))
}
}
result match {
--- a/src/Tools/jEdit/src/jedit_lib.scala Mon Jun 19 19:59:13 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Mon Jun 19 20:32:06 2017 +0200
@@ -207,13 +207,6 @@
def caret_range(text_area: TextArea): Text.Range =
point_range(text_area.getBuffer, text_area.getCaretPosition)
- def before_caret_range(text_area: TextArea, rendering: JEdit_Rendering): Text.Range =
- {
- val snapshot = rendering.snapshot
- val former_caret = snapshot.revert(text_area.getCaretPosition)
- snapshot.convert(Text.Range(former_caret - 1, former_caret))
- }
-
def visible_range(text_area: TextArea): Option[Text.Range] =
{
val buffer = text_area.getBuffer
--- a/src/Tools/jEdit/src/jedit_spell_checker.scala Mon Jun 19 19:59:13 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Mon Jun 19 20:32:06 2017 +0200
@@ -21,20 +21,14 @@
{
/* completion */
- def completion(text_area: TextArea, explicit: Boolean, rendering: JEdit_Rendering)
+ def completion(rendering: JEdit_Rendering, explicit: Boolean, caret: Text.Offset)
: Option[Completion.Result] =
{
for {
spell_checker <- PIDE.plugin.spell_checker.get
if explicit
- range = JEdit_Lib.before_caret_range(text_area, rendering)
- word <- Spell_Checker.current_word(rendering, range)
- words = spell_checker.complete(word.info)
- if words.nonEmpty
- descr = "(from dictionary " + quote(spell_checker.toString) + ")"
- items =
- words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
- } yield Completion.Result(word.range, word.info, false, items)
+ res <- spell_checker.completion(rendering, caret)
+ } yield res
}