# HG changeset patch # User wenzelm # Date 1497897126 -7200 # Node ID e6f808d1307c01e1b9c89fff31772a5ac6edb9fc # Parent dad409cd3423c205bd638cff39441698709e3b4d tuned signature; clarified modules; diff -r dad409cd3423 -r e6f808d1307c src/Pure/PIDE/rendering.scala --- 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) diff -r dad409cd3423 -r e6f808d1307c src/Pure/Tools/spell_checker.scala --- 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) + } } diff -r dad409cd3423 -r e6f808d1307c src/Tools/VSCode/src/vscode_rendering.scala --- 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 diff -r dad409cd3423 -r e6f808d1307c src/Tools/jEdit/src/bibtex_jedit.scala --- 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) diff -r dad409cd3423 -r e6f808d1307c src/Tools/jEdit/src/completion_popup.scala --- 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 { diff -r dad409cd3423 -r e6f808d1307c src/Tools/jEdit/src/jedit_lib.scala --- 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 diff -r dad409cd3423 -r e6f808d1307c src/Tools/jEdit/src/jedit_spell_checker.scala --- 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 }