# HG changeset patch
# User wenzelm
# Date 1383827924 -3600
# Node ID 232cf1e475da93f7fdec118d743eb76c6149951c
# Parent  2d61935eed4a9f2b70dca28918d2f7dbd46aa46a
tuned;

diff -r 2d61935eed4a -r 232cf1e475da src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Thu Nov 07 13:34:04 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Thu Nov 07 13:38:44 2013 +0100
@@ -376,7 +376,7 @@
 
   \begin{figure}[htb]
   \begin{center}
-  \includegraphics[scale=0.3]{output}
+  \includegraphics[width=\textwidth]{output}
   \end{center}
   \caption{Multiple views on prover output: gutter area with icon,
     text area with popup, overview area, Theories panel, Output panel}
@@ -450,7 +450,7 @@
 
   \begin{figure}[htb]
   \begin{center}
-  \includegraphics[scale=0.5]{popup1}
+  \includegraphics[scale=0.3]{popup1}
   \end{center}
   \caption{Tooltip and hyperlink for some formal entity}
   \label{fig:tooltip}
@@ -462,7 +462,7 @@
 
   \begin{figure}[htb]
   \begin{center}
-  \includegraphics[scale=0.5]{popup2}
+  \includegraphics[scale=0.3]{popup2}
   \end{center}
   \caption{Nested tooltips over formal entities}
   \label{fig:nested-tooltips}
@@ -778,7 +778,7 @@
 
   \begin{figure}[htb]
   \begin{center}
-  \includegraphics[scale=0.5]{auto-tools}
+  \includegraphics[scale=0.3]{auto-tools}
   \end{center}
   \caption{Results of automatically tried tools}
   \label{fig:auto-tools}