# HG changeset patch
# User wenzelm
# Date 1557394557 -7200
# Node ID b2eac0e8241ce8c8fe026d40f5e130318e473af1
# Parent  4ce07be8ba17d020f2ae3c0a1db17e83042baba8
more uniform scaling;

diff -r 4ce07be8ba17 -r b2eac0e8241c src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed May 08 21:28:34 2019 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Thu May 09 11:35:57 2019 +0200
@@ -64,7 +64,7 @@
 text \<open>
   \begin{figure}[!htb]
   \begin{center}
-  \includegraphics[scale=0.3]{isabelle-jedit}
+  \includegraphics[width=\textwidth]{isabelle-jedit}
   \end{center}
   \caption{The Isabelle/jEdit Prover IDE}
   \label{fig:isabelle-jedit}
@@ -1203,7 +1203,7 @@
 
   \begin{figure}[!htb]
   \begin{center}
-  \includegraphics[scale=0.5]{popup1}
+  \includegraphics[scale=0.333]{popup1}
   \end{center}
   \caption{Tooltip and hyperlink for some formal entity}
   \label{fig:tooltip}
@@ -1215,7 +1215,7 @@
 
   \begin{figure}[!htb]
   \begin{center}
-  \includegraphics[scale=0.5]{popup2}
+  \includegraphics[scale=0.333]{popup2}
   \end{center}
   \caption{Nested tooltips over formal entities}
   \label{fig:nested-tooltips}
@@ -1253,7 +1253,7 @@
 
   \begin{figure}[!htb]
   \begin{center}
-  \includegraphics[scale=0.5]{scope1}
+  \includegraphics[scale=0.333]{scope1}
   \end{center}
   \caption{Scope of formal entity: defining vs.\ referencing positions}
   \label{fig:scope1}
@@ -1266,7 +1266,7 @@
 
   \begin{figure}[!htb]
   \begin{center}
-  \includegraphics[scale=0.5]{scope2}
+  \includegraphics[scale=0.333]{scope2}
   \end{center}
   \caption{The result of semantic selection and systematic renaming}
   \label{fig:scope2}
@@ -1711,7 +1711,7 @@
 
   \begin{figure}[!htb]
   \begin{center}
-  \includegraphics[scale=0.4]{auto-tools}
+  \includegraphics[scale=0.333]{auto-tools}
   \end{center}
   \caption{Result of automatically tried tools}
   \label{fig:auto-tools}