proper navigation wrt. caret;
tuned signature;
--- a/src/Tools/jEdit/src/isabelle.scala Sun Mar 01 22:14:11 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Sun Mar 01 22:32:10 2020 +0100
@@ -542,14 +542,18 @@
/* error navigation */
private def goto_error(
- view: View, range: Text.Range, which: String = "")(get: List[Text.Markup] => Option[Text.Markup])
+ view: View,
+ range: Text.Range,
+ avoid_range: Text.Range = Text.Range.offside,
+ which: String = "")(get: List[Text.Markup] => Option[Text.Markup])
{
GUI_Thread.require {}
val text_area = view.getTextArea
for (doc_view <- Document_View.get(text_area)) {
val rendering = doc_view.get_rendering()
- get(rendering.errors(range)) match {
+ val errs = rendering.errors(range).filterNot(_.range.overlaps(avoid_range))
+ get(errs) match {
case Some(err) =>
PIDE.editor.goto_buffer(false, view, view.getBuffer, err.range.start)
case None =>
@@ -564,18 +568,17 @@
def goto_last_error(view: View): Unit =
goto_error(view, JEdit_Lib.buffer_range(view.getBuffer))(_.lastOption)
- def goto_prev_error(view: View): Unit =
- goto_error(view, JEdit_Lib.buffer_range_to_caret(view.getTextArea), which = "previous ")(
- list =>
- list.reverse match {
- case _ :: err :: _ => Some(err)
- case _ => None
- })
+ def goto_prev_error(view: View)
+ {
+ val caret_range = JEdit_Lib.caret_range(view.getTextArea)
+ val range = Text.Range(0, caret_range.stop)
+ goto_error(view, range, avoid_range = caret_range, which = "previous ")(_.lastOption)
+ }
- def goto_next_error(view: View): Unit =
- goto_error(view, JEdit_Lib.buffer_range_from_caret(view.getTextArea), which = "next ")(
- {
- case _ :: err :: _ => Some(err)
- case _ => None
- })
+ def goto_next_error(view: View)
+ {
+ val caret_range = JEdit_Lib.caret_range(view.getTextArea)
+ val range = Text.Range(caret_range.start, view.getBuffer.getLength)
+ goto_error(view, range, avoid_range = caret_range, which = "next ")(_.headOption)
+ }
}
--- a/src/Tools/jEdit/src/jedit_lib.scala Sun Mar 01 22:14:11 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Sun Mar 01 22:32:10 2020 +0100
@@ -216,12 +216,6 @@
def caret_range(text_area: TextArea): Text.Range =
point_range(text_area.getBuffer, text_area.getCaretPosition)
- def buffer_range_to_caret(text_area: TextArea): Text.Range =
- Text.Range(0, caret_range(text_area).stop)
-
- def buffer_range_from_caret(text_area: TextArea): Text.Range =
- Text.Range(caret_range(text_area).start, text_area.getBufferLength)
-
def visible_range(text_area: TextArea): Option[Text.Range] =
{
val buffer = text_area.getBuffer