--- 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}
--- a/src/Doc/JEdit/document/root.tex Wed Apr 10 23:35:25 2019 +0200
+++ b/src/Doc/JEdit/document/root.tex Wed Apr 10 23:45:20 2019 +0200
@@ -2,6 +2,7 @@
\usepackage{lmodern}
\usepackage[T1]{fontenc}
\usepackage{supertabular}
+\usepackage{rotating}
\usepackage{graphicx}
\usepackage{iman,extra,isar}
\usepackage[nohyphen,strings]{underscore}