# HG changeset patch
# User wenzelm
# Date 1583153032 -3600
# Node ID ae3399b05e9b827c986abb8736b92855a86874d9
# Parent  f2a79950748e77f16024b772aa0934b7bec2bd6c
more documentation;

diff -r f2a79950748e -r ae3399b05e9b NEWS
--- 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
diff -r f2a79950748e -r ae3399b05e9b src/Doc/JEdit/JEdit.thy
--- 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>