# HG changeset patch
# User wenzelm
# Date 1452625097 -3600
# Node ID b855771b39798fa3a5b0b88a82eeabc87e184e36
# Parent  df566b87e26925453060b2cb3d6c4278e35dd6a8
updated old screenshots, added new screenshots;

diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/JEdit.thy
--- 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>
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/auto-tools.png
Binary file src/Doc/JEdit/document/auto-tools.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/bibtex-mode.png
Binary file src/Doc/JEdit/document/bibtex-mode.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/cite-completion.png
Binary file src/Doc/JEdit/document/cite-completion.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/isabelle-jedit-hdpi.png
Binary file src/Doc/JEdit/document/isabelle-jedit-hdpi.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/isabelle-jedit.png
Binary file src/Doc/JEdit/document/isabelle-jedit.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/markdown-document.png
Binary file src/Doc/JEdit/document/markdown-document.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/ml-debugger.png
Binary file src/Doc/JEdit/document/ml-debugger.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/output-and-state.png
Binary file src/Doc/JEdit/document/output-and-state.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/output-including-state.png
Binary file src/Doc/JEdit/document/output-including-state.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/output.png
Binary file src/Doc/JEdit/document/output.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/popup1.png
Binary file src/Doc/JEdit/document/popup1.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/popup2.png
Binary file src/Doc/JEdit/document/popup2.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/query.png
Binary file src/Doc/JEdit/document/query.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/sidekick-document.png
Binary file src/Doc/JEdit/document/sidekick-document.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/sidekick.png
Binary file src/Doc/JEdit/document/sidekick.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/sledgehammer.png
Binary file src/Doc/JEdit/document/sledgehammer.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/JEdit/document/theories.png
Binary file src/Doc/JEdit/document/theories.png has changed
diff -r df566b87e269 -r b855771b3979 src/Doc/ROOT
--- 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"