# HG changeset patch
# User wenzelm
# Date 1554932720 -7200
# Node ID 7721589f3efdc334d86655ed3ad3d08cc44938ff
# Parent  2337a6bc5e4128644eba1b8f651003e37cd17830
tuned layout;

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}
diff -r 2337a6bc5e41 -r 7721589f3efd src/Doc/JEdit/document/root.tex
--- 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}