equal
deleted
inserted
replaced
334 |
334 |
335 Users may experiment with different Swing look-and-feels, but need to keep |
335 Users may experiment with different Swing look-and-feels, but need to keep |
336 in mind that this extra variance of GUI functionality is unlikely to work in |
336 in mind that this extra variance of GUI functionality is unlikely to work in |
337 arbitrary combinations. The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> |
337 arbitrary combinations. The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> |
338 should always work on all platforms, although they are technically and |
338 should always work on all platforms, although they are technically and |
339 stylistically outdated. The historic \<^emph>\<open>CDE/Motif\<close> on Linux should be |
339 stylistically outdated. The historic \<^emph>\<open>CDE/Motif\<close> should be ignored. |
340 ignored. |
|
341 |
340 |
342 After changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close>, |
341 After changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close>, |
343 Isabelle/jEdit should be restarted to take full effect. |
342 Isabelle/jEdit should be restarted to take full effect. |
344 \<close> |
343 \<close> |
345 |
344 |