more uniform scaling;
authorwenzelm
Thu May 09 11:35:57 2019 +0200 (6 months ago)
changeset 70251b2eac0e8241c
parent 70249 4ce07be8ba17
child 70252 236c1bb128da
more uniform scaling;
src/Doc/JEdit/JEdit.thy
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Wed May 08 21:28:34 2019 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu May 09 11:35:57 2019 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4  text \<open>
     1.5    \begin{figure}[!htb]
     1.6    \begin{center}
     1.7 -  \includegraphics[scale=0.3]{isabelle-jedit}
     1.8 +  \includegraphics[width=\textwidth]{isabelle-jedit}
     1.9    \end{center}
    1.10    \caption{The Isabelle/jEdit Prover IDE}
    1.11    \label{fig:isabelle-jedit}
    1.12 @@ -1203,7 +1203,7 @@
    1.13  
    1.14    \begin{figure}[!htb]
    1.15    \begin{center}
    1.16 -  \includegraphics[scale=0.5]{popup1}
    1.17 +  \includegraphics[scale=0.333]{popup1}
    1.18    \end{center}
    1.19    \caption{Tooltip and hyperlink for some formal entity}
    1.20    \label{fig:tooltip}
    1.21 @@ -1215,7 +1215,7 @@
    1.22  
    1.23    \begin{figure}[!htb]
    1.24    \begin{center}
    1.25 -  \includegraphics[scale=0.5]{popup2}
    1.26 +  \includegraphics[scale=0.333]{popup2}
    1.27    \end{center}
    1.28    \caption{Nested tooltips over formal entities}
    1.29    \label{fig:nested-tooltips}
    1.30 @@ -1253,7 +1253,7 @@
    1.31  
    1.32    \begin{figure}[!htb]
    1.33    \begin{center}
    1.34 -  \includegraphics[scale=0.5]{scope1}
    1.35 +  \includegraphics[scale=0.333]{scope1}
    1.36    \end{center}
    1.37    \caption{Scope of formal entity: defining vs.\ referencing positions}
    1.38    \label{fig:scope1}
    1.39 @@ -1266,7 +1266,7 @@
    1.40  
    1.41    \begin{figure}[!htb]
    1.42    \begin{center}
    1.43 -  \includegraphics[scale=0.5]{scope2}
    1.44 +  \includegraphics[scale=0.333]{scope2}
    1.45    \end{center}
    1.46    \caption{The result of semantic selection and systematic renaming}
    1.47    \label{fig:scope2}
    1.48 @@ -1711,7 +1711,7 @@
    1.49  
    1.50    \begin{figure}[!htb]
    1.51    \begin{center}
    1.52 -  \includegraphics[scale=0.4]{auto-tools}
    1.53 +  \includegraphics[scale=0.333]{auto-tools}
    1.54    \end{center}
    1.55    \caption{Result of automatically tried tools}
    1.56    \label{fig:auto-tools}