src/Doc/JEdit/JEdit.thy
changeset 68737 a8bef9ff7dc0
parent 68736 29dbf3408021
child 69343 395c4fb15ea2
equal deleted inserted replaced
68736:29dbf3408021 68737:a8bef9ff7dc0
  1905 
  1905 
  1906   \begin{figure}[!htb]
  1906   \begin{figure}[!htb]
  1907   \begin{center}
  1907   \begin{center}
  1908   \includegraphics[scale=0.333]{bibtex-mode}
  1908   \includegraphics[scale=0.333]{bibtex-mode}
  1909   \end{center}
  1909   \end{center}
  1910   \caption{Bib{\TeX} mode with context menu and SideKick tree view}
  1910   \caption{Bib{\TeX} mode with context menu, SideKick tree view, and
       
  1911     semantic output from the \<^verbatim>\<open>bibtex\<close> tool}
  1911   \label{fig:bibtex-mode}
  1912   \label{fig:bibtex-mode}
  1912   \end{figure}
  1913   \end{figure}
  1913 
  1914 
  1914   Regular document preview (\secref{sec:document-preview}) of \<^verbatim>\<open>.bib\<close> files
  1915   Regular document preview (\secref{sec:document-preview}) of \<^verbatim>\<open>.bib\<close> files
  1915   approximates the usual {\LaTeX} bibliography output in HTML (using style
  1916   approximates the usual {\LaTeX} bibliography output in HTML (using style