src/Doc/JEdit/JEdit.thy
changeset 68737 a8bef9ff7dc0
parent 68736 29dbf3408021
child 69343 395c4fb15ea2
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Mon Aug 06 14:29:46 2018 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon Aug 06 15:19:39 2018 +0200
     1.3 @@ -1907,7 +1907,8 @@
     1.4    \begin{center}
     1.5    \includegraphics[scale=0.333]{bibtex-mode}
     1.6    \end{center}
     1.7 -  \caption{Bib{\TeX} mode with context menu and SideKick tree view}
     1.8 +  \caption{Bib{\TeX} mode with context menu, SideKick tree view, and
     1.9 +    semantic output from the \<^verbatim>\<open>bibtex\<close> tool}
    1.10    \label{fig:bibtex-mode}
    1.11    \end{figure}
    1.12