--- a/src/Doc/JEdit/JEdit.thy Tue Jan 12 15:43:26 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy Tue Jan 12 19:58:17 2016 +0100
@@ -948,6 +948,29 @@
\<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>
@@ -967,7 +990,7 @@
\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}
@@ -1655,6 +1678,22 @@
\<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>
@@ -1694,6 +1733,22 @@
\<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>
Binary file src/Doc/JEdit/document/auto-tools.png has changed
Binary file src/Doc/JEdit/document/bibtex-mode.png has changed
Binary file src/Doc/JEdit/document/cite-completion.png has changed
Binary file src/Doc/JEdit/document/isabelle-jedit-hdpi.png has changed
Binary file src/Doc/JEdit/document/isabelle-jedit.png has changed
Binary file src/Doc/JEdit/document/markdown-document.png has changed
Binary file src/Doc/JEdit/document/ml-debugger.png has changed
Binary file src/Doc/JEdit/document/output-and-state.png has changed
Binary file src/Doc/JEdit/document/output-including-state.png has changed
Binary file src/Doc/JEdit/document/output.png has changed
Binary file src/Doc/JEdit/document/popup1.png has changed
Binary file src/Doc/JEdit/document/popup2.png has changed
Binary file src/Doc/JEdit/document/query.png has changed
Binary file src/Doc/JEdit/document/sidekick-document.png has changed
Binary file src/Doc/JEdit/document/sidekick.png has changed
Binary file src/Doc/JEdit/document/sledgehammer.png has changed
Binary file src/Doc/JEdit/document/theories.png has changed
--- a/src/Doc/ROOT Tue Jan 12 15:43:26 2016 +0100
+++ b/src/Doc/ROOT Tue Jan 12 19:58:17 2016 +0100
@@ -207,15 +207,19 @@
"bibtex-mode.png"
"build"
"cite-completion.png"
+ "isabelle-jedit-hdpi.png"
"isabelle-jedit.png"
- "isabelle-jedit-hdpi.png"
+ "markdown-document.png"
+ "ml-debugger.png"
+ "output-and-state.png"
+ "output-including-state.png"
"output.png"
- "query.png"
"popup1.png"
"popup2.png"
+ "query.png"
"root.tex"
+ "sidekick-document.png"
"sidekick.png"
- "sidekick-document.png"
"sledgehammer.png"
"theories.png"