diff -r 2337a6bc5e41 -r 7721589f3efd src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed Apr 10 23:35:25 2019 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Wed Apr 10 23:45:20 2019 +0200
@@ -410,13 +410,13 @@
   pixels. This leads to decent rendering quality, despite the old-fashioned
   appearance of \<^emph>\<open>Metal\<close>.
 
-  \begin{figure}[!htb]
+  \begin{sidewaysfigure}[!htb]
   \begin{center}
   \includegraphics[width=\textwidth]{isabelle-jedit-hdpi}
   \end{center}
   \caption{Metal look-and-feel with custom fonts for very high resolution}
   \label{fig:isabelle-jedit-hdpi}
-  \end{figure}
+  \end{sidewaysfigure}
 \<close>
 
 
@@ -1711,7 +1711,7 @@
 
   \begin{figure}[!htb]
   \begin{center}
-  \includegraphics[scale=0.333]{auto-tools}
+  \includegraphics[scale=0.4]{auto-tools}
   \end{center}
   \caption{Result of automatically tried tools}
   \label{fig:auto-tools}