src/Doc/JEdit/JEdit.thy

   \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate certain
   actions (see \secref{sec:auto-tools} and \secref{sec:sledgehammer}).
 \<close>
 
 
+section \<open>Proof state output \label{sec:state-output}\<close>
+
+text \<open>
+  FIXME
+  \figref{fig:output-and-state} versus \figref{fig:output-including-state}
+
+  \begin{figure}[htb]
+  \begin{center}
+  \includegraphics[scale=0.333]{output-and-state}
+  \end{center}
+  \caption{Separate proof state display (right) and other output (bottom).}
+  \label{fig:output-and-state}
+  \end{figure}
+
+  \begin{figure}[htb]
+  \begin{center}
+  \includegraphics[scale=0.333]{output-including-state}
+  \end{center}
+  \caption{Proof state display within the regular output panel}
+  \label{fig:output-including-state}
+  \end{figure}
+\<close>
+
 section \<open>Query \label{sec:query}\<close>
 
 text \<open>
   The \<^emph>\<open>Query\<close> panel provides various GUI forms to request extra information
   from the prover. In old times the user would have issued some diagnostic

 
   \begin{figure}[htb]
   \begin{center}
   \includegraphics[scale=0.333]{query}
   \end{center}
-  \caption{An instance of the Query panel}
+  \caption{An instance of the Query panel: find theorems}
   \label{fig:query}
   \end{figure}
 
   \<^medskip>
   The following GUI elements are common to all query modes:

   proofs. The alternative mode \<^verbatim>\<open>sidekick\<close> uses the document structure of the
   SideKick parser, as explained above.
 \<close>
 
 
+section \<open>Markdown structure\<close>
+
+text \<open>
+  FIXME
+  \figref{fig:markdown-document}
+
+  \begin{figure}[htb]
+  \begin{center}
+  \includegraphics[scale=0.333]{markdown-document}
+  \end{center}
+  \caption{Markdown structure within document text}
+  \label{fig:markdown-document}
+  \end{figure}
+\<close>
+
+
 section \<open>Citations and Bib{\TeX} entries\<close>
 
 text \<open>
   Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\<open>.bib\<close> files. The
   Isabelle session build process and the @{tool latex} tool @{cite

   \label{fig:bibtex-mode}
   \end{figure}
 \<close>
 
 
+chapter \<open>ML debugger\<close>
+
+text \<open>
+  FIXME
+  \figref{fig:ml-debugger}
+
+  \begin{figure}[htb]
+  \begin{center}
+  \includegraphics[scale=0.333]{ml-debugger}
+  \end{center}
+  \caption{ML debugger}
+  \label{fig:ml-debugger}
+  \end{figure}
+\<close>
+
+
 chapter \<open>Miscellaneous tools\<close>
 
 section \<open>Timing\<close>
 
 text \<open>