--- a/NEWS Mon Mar 02 13:43:39 2020 +0100
+++ b/NEWS Mon Mar 02 13:43:52 2020 +0100
@@ -63,9 +63,9 @@
document snapshot:
isabelle.first-error (CS+a)
- isabelle-last-error (CS+z)
- isabelle-next-error (CS+n)
- isabelle-prev-error (CS+p)
+ 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
--- a/src/Doc/JEdit/JEdit.thy Mon Mar 02 13:43:39 2020 +0100
+++ b/src/Doc/JEdit/JEdit.thy Mon Mar 02 13:43:52 2020 +0100
@@ -1074,6 +1074,23 @@
recursively via further popups and hyperlinks (see
\secref{sec:tooltips-hyperlinks}), or clicked directly to initiate certain
actions (see \secref{sec:auto-tools} and \secref{sec:sledgehammer}).
+
+ \<^medskip>
+ Alternatively, the subsequent actions (with keyboard shortcuts) allow to
+ show tooltip messages or navigate error positions:
+
+ \<^medskip>
+ \begin{tabular}[t]{l}
+ @{action_ref "isabelle.tooltip"} (\<^verbatim>\<open>CS+b\<close>) \\
+ @{action_ref "isabelle.message"} (\<^verbatim>\<open>CS+m\<close>) \\
+ \end{tabular}\quad
+ \begin{tabular}[t]{l}
+ @{action_ref "isabelle.first-error"} (\<^verbatim>\<open>CS+a\<close>) \\
+ @{action_ref "isabelle.last-error"} (\<^verbatim>\<open>CS+z\<close>) \\
+ @{action_ref "isabelle.next-error"} (\<^verbatim>\<open>CS+n\<close>) \\
+ @{action_ref "isabelle.prev-error"} (\<^verbatim>\<open>CS+p\<close>) \\
+ \end{tabular}
+ \<^medskip>
\<close>