# HG changeset patch
# User wenzelm
# Date 1583098330 -3600
# Node ID f61e55bab00c0cdc3a24104f54b0d86ff0ad3188
# Parent  248402f42cace49466139ed41842d1dcb562d769
proper navigation wrt. caret;
tuned signature;

diff -r 248402f42cac -r f61e55bab00c src/Tools/jEdit/src/isabelle.scala
--- 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)
+  }
 }
diff -r 248402f42cac -r f61e55bab00c src/Tools/jEdit/src/jedit_lib.scala
--- 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