269 \<close> |
269 \<close> |
270 |
270 |
271 |
271 |
272 chapter \<open>Augmented jEdit functionality\<close> |
272 chapter \<open>Augmented jEdit functionality\<close> |
273 |
273 |
274 section \<open>Look-and-feel\<close> |
274 section \<open>GUI rendering\<close> |
275 |
275 |
276 text \<open>jEdit is a Java/AWT/Swing application with some ambition to |
276 subsection \<open>Look-and-feel \label{sec:look-and-feel}\<close> |
277 support ``native'' look-and-feel on all platforms, within the limits |
277 |
278 of what Oracle as Java provider and major operating system |
278 text \<open> |
279 distributors allow (see also \secref{sec:problems}). |
279 jEdit is a Java/AWT/Swing application with some ambition to support |
|
280 ``native'' look-and-feel on all platforms, within the limits of what Oracle |
|
281 as Java provider and major operating system distributors allow (see also |
|
282 \secref{sec:problems}). |
280 |
283 |
281 Isabelle/jEdit enables platform-specific look-and-feel by default as |
284 Isabelle/jEdit enables platform-specific look-and-feel by default as |
282 follows. |
285 follows. |
283 |
286 |
284 \begin{description} |
287 \begin{description} |
314 \emph{Nimbus} and \emph{Metal} should always work. The historic |
317 \emph{Nimbus} and \emph{Metal} should always work. The historic |
315 \emph{CDE/Motif} is better ignore altogether. |
318 \emph{CDE/Motif} is better ignore altogether. |
316 |
319 |
317 After changing the look-and-feel in \emph{Global Options~/ |
320 After changing the look-and-feel in \emph{Global Options~/ |
318 Appearance}, it is advisable to restart Isabelle/jEdit in order to |
321 Appearance}, it is advisable to restart Isabelle/jEdit in order to |
319 take full effect.\<close> |
322 take full effect. |
|
323 \<close> |
|
324 |
|
325 |
|
326 subsection \<open>Displays with very high resolution \label{sec:hdpi}\<close> |
|
327 |
|
328 text \<open> |
|
329 Many years ago, displays with $1024 \times 768$ or $1280 \times 1024$ pixels |
|
330 were considered ``high resolution'' and bitmap fonts with 12 or 14 pixels as |
|
331 adequate for text rendering. Today (2015), we routinely see ``Full HD'' |
|
332 monitors at $1920 \times 1080$ pixels, and occasionally ``Ultra HD'' at |
|
333 $3840 \times 2160$ or more, but GUI rendering did not really progress |
|
334 beyond the old standards. |
|
335 |
|
336 Isabelle/jEdit defaults are a compromise for reasonable out-of-the box |
|
337 results on common platforms and medium resolution displays (e.g.\ the ``Full |
|
338 HD'' category). Subsequently there are further hints to improve on that. |
|
339 |
|
340 \medskip The \textbf{operating-system platform} usually provides some |
|
341 configuration for global scaling of text fonts, e.g.\ $120\%$--$250\%$ on |
|
342 Windows. Changing that only has a partial effect on GUI rendering; |
|
343 satisfactory display quality requires further adjustments. |
|
344 |
|
345 \medskip The Isabelle/jEdit \textbf{application} and its plugins provide |
|
346 various font properties that are summarized below. |
|
347 |
|
348 \begin{itemize} |
|
349 |
|
350 \item \emph{Global Options / Text Area / Text font}: the main text area |
|
351 font, which is also used as reference point for various derived font sizes, |
|
352 e.g.\ the Output panel (\secref{sec:output}). |
|
353 |
|
354 \item \emph{Global Options / Gutter / Gutter font}: the font for the gutter |
|
355 area left of the main text area, e.g.\ relevant for display of line numbers |
|
356 (disabled by default). |
|
357 |
|
358 \item \emph{Global Options / Appearance / Button, menu and label font} as |
|
359 well as \emph{List and text field font}: this specifies the primary and |
|
360 secondary font for the old \emph{Metal} look-and-feel |
|
361 (\secref{sec:look-and-feel}), which happens to scale better than newer ones |
|
362 like \emph{Nimbus}. |
|
363 |
|
364 \item \emph{Plugin Options / Isabelle / General / Reset Font Size}: the main |
|
365 text area font size for action @{action_ref "isabelle.reset-font-size"}, |
|
366 e.g.\ relevant for quick scaling like in major web browsers. |
|
367 |
|
368 \item \emph{Plugin Options / Console / General / Font}: the console window |
|
369 font, e.g.\ relevant for Isabelle/Scala command-line. |
|
370 |
|
371 \end{itemize} |
|
372 |
|
373 In \figref{fig:isabelle-jedit-hdpi} the \emph{Metal} look-and-feel is |
|
374 configured with custom fonts at 30 pixels, and the main text area and |
|
375 console at 36 pixels. Despite the old-fashioned appearance of \emph{Metal}, |
|
376 this leads to decent rendering quality on all platforms. |
|
377 |
|
378 \begin{figure}[htb] |
|
379 \begin{center} |
|
380 \includegraphics[width=\textwidth]{isabelle-jedit-hdpi} |
|
381 \end{center} |
|
382 \caption{Metal look-and-feel with custom fonts for very high resolution} |
|
383 \label{fig:isabelle-jedit-hdpi} |
|
384 \end{figure} |
|
385 |
|
386 On Linux, it is also possible to use \emph{GTK+} with a suitable theme and |
|
387 global font scaling. On Mac OS X, the default setup for ``Retina'' displays |
|
388 should work adequately with the native look-and-feel. |
|
389 \<close> |
320 |
390 |
321 |
391 |
322 section \<open>Dockable windows \label{sec:dockables}\<close> |
392 section \<open>Dockable windows \label{sec:dockables}\<close> |
323 |
393 |
324 text \<open> |
394 text \<open> |
1793 desktop environments (like Gnome) disrupt the handling of menu popups and |
1863 desktop environments (like Gnome) disrupt the handling of menu popups and |
1794 mouse positions of Java/AWT/Swing. |
1864 mouse positions of Java/AWT/Swing. |
1795 |
1865 |
1796 \textbf{Workaround:} Use mainstream versions of Linux desktops. |
1866 \textbf{Workaround:} Use mainstream versions of Linux desktops. |
1797 |
1867 |
|
1868 \item \textbf{Problem:} Native Windows look-and-feel with global font |
|
1869 scaling leads to bad GUI rendering of various list views, e.g.\ the |
|
1870 \emph{Documentation} panel. |
|
1871 |
|
1872 \textbf{Workaround:} Use \emph{Metal} look-and-feel and re-adjust its |
|
1873 primary and secondary font as explained in \secref{sec:hdpi}. |
|
1874 |
1798 \item \textbf{Problem:} Full-screen mode via jEdit action @{action_ref |
1875 \item \textbf{Problem:} Full-screen mode via jEdit action @{action_ref |
1799 "toggle-full-screen"} (default keyboard shortcut @{verbatim F11}) works on |
1876 "toggle-full-screen"} (default keyboard shortcut @{verbatim F11}) works on |
1800 Windows, but not on Mac OS X or various Linux/X11 window managers. |
1877 Windows, but not on Mac OS X or various Linux/X11 window managers. |
1801 |
1878 |
1802 \textbf{Workaround:} Use native full-screen control of the window |
1879 \textbf{Workaround:} Use native full-screen control of the window |