--- a/NEWS Sun Mar 01 15:20:47 2020 +0100
+++ b/NEWS Sun Mar 01 21:52:21 2020 +0100
@@ -59,6 +59,14 @@
tooltip message popups, corresponding to mouse hovering with/without the
CONTROL/COMMAND key pressed.
+* The following actions allow to navigate errors within the current
+document snapshot:
+
+ isabelle.first-error (CS+a)
+ isabelle-last-error (CS+z)
+ isabelle-next-error (CS+n)
+ isabelle-prev-error (CS+p)
+
* Prover IDE startup is now much faster, because theory dependencies are
no longer explored in advance. The overall session structure with its
declarations of 'directories' is sufficient to locate theory files. Thus
--- a/src/Pure/PIDE/rendering.scala Sun Mar 01 15:20:47 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala Sun Mar 01 21:52:21 2020 +0100
@@ -208,6 +208,9 @@
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
Markup.BAD)
+ val warning_elements = Markup.Elements(Markup.WARNING, Markup.LEGACY)
+ val error_elements = Markup.Elements(Markup.ERROR)
+
val caret_focus_elements = Markup.Elements(Markup.ENTITY)
val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
@@ -653,6 +656,15 @@
}
+ /* messages */
+
+ def warnings(range: Text.Range): List[Text.Markup] =
+ snapshot.select(range, Rendering.warning_elements, _ => Some(_)).map(_.info)
+
+ def errors(range: Text.Range): List[Text.Markup] =
+ snapshot.select(range, Rendering.error_elements, _ => Some(_)).map(_.info)
+
+
/* command status overview */
def overview_color(range: Text.Range): Option[Rendering.Color.Value] =
--- a/src/Tools/jEdit/src/actions.xml Sun Mar 01 15:20:47 2020 +0100
+++ b/src/Tools/jEdit/src/actions.xml Sun Mar 01 21:52:21 2020 +0100
@@ -87,6 +87,26 @@
isabelle.jedit.Isabelle.show_tooltip(view, false);
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.first-error">
+ <CODE>
+ isabelle.jedit.Isabelle.goto_first_error(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.last-error">
+ <CODE>
+ isabelle.jedit.Isabelle.goto_last_error(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.prev-error">
+ <CODE>
+ isabelle.jedit.Isabelle.goto_prev_error(view);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.next-error">
+ <CODE>
+ isabelle.jedit.Isabelle.goto_next_error(view);
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.complete-word">
<CODE>
isabelle.jedit.Isabelle.complete(view, true);
--- a/src/Tools/jEdit/src/isabelle.scala Sun Mar 01 15:20:47 2020 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Sun Mar 01 21:52:21 2020 +0100
@@ -537,4 +537,45 @@
Pretty_Tooltip(view, painter, loc, rendering, results, tip)
}
}
+
+
+ /* error navigation */
+
+ private def goto_error(
+ view: View, range: Text.Range, 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 {
+ case Some(err) =>
+ PIDE.editor.goto_buffer(false, view, view.getBuffer, err.range.start)
+ case None =>
+ view.getStatus.setMessageAndClear("No " + which + "error in current document snapshot")
+ }
+ }
+ }
+
+ def goto_first_error(view: View): Unit =
+ goto_error(view, JEdit_Lib.buffer_range(view.getBuffer))(_.headOption)
+
+ 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_next_error(view: View): Unit =
+ goto_error(view, JEdit_Lib.buffer_range_from_caret(view.getTextArea), which = "next ")(
+ {
+ case _ :: err :: _ => Some(err)
+ case _ => None
+ })
}
--- a/src/Tools/jEdit/src/jEdit.props Sun Mar 01 15:20:47 2020 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Sun Mar 01 21:52:21 2020 +0100
@@ -222,6 +222,8 @@
isabelle.draft.label=Show draft in browser
isabelle.exclude-word-permanently.label=Exclude word permanently
isabelle.exclude-word.label=Exclude word
+isabelle.first-error.label=Go to first error
+isabelle.first-error.shortcut=CS+a
isabelle.include-word-permanently.label=Include word permanently
isabelle.include-word.label=Include word
isabelle.increase-font-size.label=Increase font size
@@ -229,11 +231,17 @@
isabelle.increase-font-size.shortcut=C+PLUS
isabelle.increase-font-size2.label=Increase font size (clone)
isabelle.increase-font-size2.shortcut=C+EQUALS
+isabelle.last-error.label=Go to last error
+isabelle.last-error.shortcut=CS+z
isabelle.message.label=Show message
isabelle.message.shortcut=CS+m
isabelle.newline.label=Newline with indentation of Isabelle keywords
isabelle.newline.shortcut=ENTER
+isabelle.next-error.label=Go to next error
+isabelle.next-error.shortcut=CS+n
isabelle.options.label=Isabelle options
+isabelle.prev-error.label=Go to previous error
+isabelle.prev-error.shortcut=CS+p
isabelle.preview.label=Show preview in browser
isabelle.reset-continuous-checking.label=Reset continuous checking
isabelle.reset-font-size.label=Reset font size
--- a/src/Tools/jEdit/src/jedit_lib.scala Sun Mar 01 15:20:47 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Sun Mar 01 21:52:21 2020 +0100
@@ -216,6 +216,12 @@
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