--- a/src/Tools/jEdit/src/completion_popup.scala Tue Apr 15 11:26:17 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Tue Apr 15 12:34:16 2014 +0200
@@ -126,9 +126,8 @@
active_range match {
case Some(range) => range.try_restrict(line_range)
case None =>
- val buffer = text_area.getBuffer
if (line_range.contains(text_area.getCaretPosition)) {
- JEdit_Lib.before_caret_range(text_area, rendering).try_restrict(line_range) match {
+ JEdit_Lib.before_caret_range(text_area, rendering) match {
case Some(range) if !range.is_singularity =>
rendering.semantic_completion(range) match {
case Some(Text.Info(_, Completion.No_Completion)) => None
@@ -164,11 +163,11 @@
val line_text = buffer.getSegment(line_start, line_length)
val context =
- (opt_rendering match {
- case Some(rendering) =>
- rendering.language_context(JEdit_Lib.before_caret_range(text_area, rendering))
- case None => None
- }) getOrElse syntax.language_context
+ (for {
+ rendering <- opt_rendering
+ range <- JEdit_Lib.before_caret_range(text_area, rendering)
+ context <- rendering.language_context(range)
+ } yield context) getOrElse syntax.language_context
syntax.completion.complete(
history, decode, explicit, line_start, line_text, caret - line_start, false, context)
@@ -181,23 +180,17 @@
/* spell-checker completion */
def spell_checker_completion(rendering: Rendering): Option[Completion.Result] =
- PIDE.spell_checker.get match {
- case Some(spell_checker) =>
- val caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
- Spell_Checker.current_word(text_area, rendering, caret_range) match {
- case Some(Text.Info(range, original)) =>
- val words = spell_checker.complete(original)
- if (words.isEmpty) None
- else {
- val descr = "(from dictionary " + quote(spell_checker.toString) + ")"
- val items = words.map(word =>
- Completion.Item(range, original, "", List(word, descr), word, 0, false))
- Some(Completion.Result(range, original, false, items))
- }
- case None => None
- }
- case None => None
- }
+ {
+ for {
+ spell_checker <- PIDE.spell_checker.get
+ caret_range <- JEdit_Lib.before_caret_range(text_area, rendering)
+ Text.Info(range, original) <- Spell_Checker.current_word(text_area, rendering, caret_range)
+ words = spell_checker.complete(original)
+ if !words.isEmpty
+ descr = "(from dictionary " + quote(spell_checker.toString) + ")"
+ items = words.map(w => Completion.Item(range, original, "", List(w, descr), w, 0, false))
+ } yield Completion.Result(range, original, false, items)
+ }
/* completion action: text area */
@@ -313,23 +306,24 @@
case Some(doc_view) =>
val rendering = doc_view.get_rendering()
val (no_completion, result) =
- rendering.semantic_completion(JEdit_Lib.before_caret_range(text_area, rendering))
- match {
- case Some(Text.Info(_, Completion.No_Completion)) =>
- (true, None)
- case Some(Text.Info(range, names: Completion.Names)) =>
- val result =
- JEdit_Lib.try_get_text(buffer, range) match {
- case Some(original) => names.complete(range, history, decode, original)
- case None => None
- }
- (false, result)
- case None =>
- (false, None)
+ JEdit_Lib.before_caret_range(text_area, rendering) match {
+ case Some(caret_range) =>
+ rendering.semantic_completion(caret_range) match {
+ case Some(Text.Info(_, Completion.No_Completion)) =>
+ (true, None)
+ case Some(Text.Info(range, names: Completion.Names)) =>
+ val result =
+ JEdit_Lib.try_get_text(buffer, range) match {
+ case Some(original) => names.complete(range, history, decode, original)
+ case None => None
+ }
+ (false, result)
+ case None => (false, None)
+ }
+ case None => (false, None)
}
(no_completion, result, Some(rendering))
- case None =>
- (false, None, None)
+ case None => (false, None, None)
}
}
if (no_completion) false
@@ -339,8 +333,8 @@
val result0 =
if (word_only) None
else
- Completion.Result.merge(history,
- semantic_completion, syntax_completion(history, explicit, opt_rendering))
+ Completion.Result.merge(history, semantic_completion,
+ syntax_completion(history, explicit, opt_rendering))
opt_rendering match {
case None => result0
case Some(rendering) =>
--- a/src/Tools/jEdit/src/jedit_lib.scala Tue Apr 15 11:26:17 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Tue Apr 15 12:34:16 2014 +0200
@@ -126,7 +126,8 @@
def jedit_views(): Iterator[View] = jEdit.getViews().iterator
def jedit_text_areas(view: View): Iterator[JEditTextArea] =
- view.getEditPanes().iterator.map(_.getTextArea)
+ if (view == null) Iterator.empty
+ else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null)
def jedit_text_areas(): Iterator[JEditTextArea] =
jedit_views().flatMap(jedit_text_areas(_))
@@ -176,21 +177,22 @@
}
- /* caret */
-
- def before_caret_range(text_area: TextArea, rendering: Rendering): Text.Range =
- {
- val snapshot = rendering.snapshot
- val former_caret = snapshot.revert(text_area.getCaretPosition)
- snapshot.convert(Text.Range(former_caret - 1, former_caret))
- }
-
-
/* text ranges */
def buffer_range(buffer: JEditBuffer): Text.Range =
Text.Range(0, buffer.getLength)
+ def line_range(buffer: JEditBuffer, line: Int): Text.Range =
+ Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line))
+
+ def before_caret_range(text_area: TextArea, rendering: Rendering): Option[Text.Range] =
+ {
+ val range = line_range(text_area.getBuffer, text_area.getCaretLine)
+ val snapshot = rendering.snapshot
+ val former_caret = snapshot.revert(text_area.getCaretPosition)
+ snapshot.convert(Text.Range(former_caret - 1, former_caret)).try_restrict(range)
+ }
+
def visible_range(text_area: TextArea): Option[Text.Range] =
{
val buffer = text_area.getBuffer