# HG changeset patch
# User wenzelm
# Date 1533561579 -7200
# Node ID a8bef9ff7dc0dbe72f92aeb9286dca82a6e544c6
# Parent  29dbf3408021ed1b33cfb2c1fd804995479a6b52
updated screenshot;

diff -r 29dbf3408021 -r a8bef9ff7dc0 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Mon Aug 06 14:29:46 2018 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Mon Aug 06 15:19:39 2018 +0200
@@ -1907,7 +1907,8 @@
   \begin{center}
   \includegraphics[scale=0.333]{bibtex-mode}
   \end{center}
-  \caption{Bib{\TeX} mode with context menu and SideKick tree view}
+  \caption{Bib{\TeX} mode with context menu, SideKick tree view, and
+    semantic output from the \<^verbatim>\<open>bibtex\<close> tool}
   \label{fig:bibtex-mode}
   \end{figure}
 
diff -r 29dbf3408021 -r a8bef9ff7dc0 src/Doc/JEdit/document/bibtex-mode.png
Binary file src/Doc/JEdit/document/bibtex-mode.png has changed