# HG changeset patch
# User wenzelm
# Date 1607863490 -3600
# Node ID 4e63acc435bd47e2b0e9ee4d5737ef31441e6613
# Parent  dc9f43a9ad232be1006c78a81e8a38c78cb801cd
minor updates on look-and-feel;

diff -r dc9f43a9ad23 -r 4e63acc435bd src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sun Dec 13 13:39:36 2020 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sun Dec 13 13:44:50 2020 +0100
@@ -332,25 +332,19 @@
 
     \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by default.
 
-    The Linux-specific \<^emph>\<open>GTK+\<close> often works, but the overall GTK theme and
-    options need to be selected to suite Java/AWT/Swing. Note that the Java
-    Virtual Machine has no direct influence of GTK rendering.
-
-    \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default.
-
-    \<^descr>[macOS:] Regular \<^emph>\<open>Mac OS X\<close> is used by default.
-
-    The bundled \<^emph>\<open>MacOSX\<close> plugin provides various functions that are expected
-    from applications on that particular platform: quit from menu or dock,
-    preferences menu, drag-and-drop of text files on the application,
-    full-screen mode for main editor windows. It is advisable to have the
-    \<^emph>\<open>MacOSX\<close> plugin enabled all the time on that platform.
+    The Linux-specific \<^emph>\<open>GTK+\<close> look-and-feel often works, but the overall GTK
+    theme and options need to be selected to suite Java/AWT/Swing. Note that
+    the Java Virtual Machine has no direct influence of GTK rendering: it
+    happens within external C libraries.
+
+    \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> look-and-feel is used by default.
+
+    \<^descr>[macOS:] Regular \<^emph>\<open>Mac OS X\<close> look-and-feel is used by default.
 
   Users may experiment with different Swing look-and-feels, but need to keep
   in mind that this extra variance of GUI functionality often causes problems.
-  The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> should always work on all
-  platforms, although they are technically and stylistically outdated. The
-  historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
+  The platform-independent \<^emph>\<open>Metal\<close> look-and-feel should work smoothly on all
+  platforms, although its is technically and stylistically outdated.
 
   Changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close> may update the
   GUI only partially: a proper restart of Isabelle/jEdit is usually required.