# HG changeset patch # User wenzelm # Date 1397558056 -7200 # Node ID 83777a91f5decf2830e4276a2c247a7a4e17d9de # Parent 5ef60881681d2df1d0081f058eb4a57651428fd2 clarified before_caret_range: prevent continuation on next line; more robust jedit_text_areas in unclear situations of object initialization; diff -r 5ef60881681d -r 83777a91f5de src/Tools/jEdit/src/completion_popup.scala --- 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) => diff -r 5ef60881681d -r 83777a91f5de src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Tue Apr 15 11:26:17 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle.scala Tue Apr 15 12:34:16 2014 +0200 @@ -299,7 +299,7 @@ spell_checker <- PIDE.spell_checker.get doc_view <- PIDE.document_view(text_area) rendering = doc_view.get_rendering() - range = JEdit_Lib.before_caret_range(text_area, rendering) + range <- JEdit_Lib.before_caret_range(text_area, rendering) Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range) } { spell_checker.update(word, include, permanent) diff -r 5ef60881681d -r 83777a91f5de src/Tools/jEdit/src/jedit_lib.scala --- 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