# HG changeset patch
# User wenzelm
# Date 1481042326 -3600
# Node ID 964ac7439a5227482fa0aeb8df61dc315b0c41a9
# Parent  8b187a7a9776dbad9fd532232305e14259d077dc
notes on whitespace;

diff -r 8b187a7a9776 -r 964ac7439a52 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Tue Dec 06 17:23:54 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Tue Dec 06 17:38:46 2016 +0100
@@ -723,6 +723,11 @@
 
   The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
   Isabelle / General\<close>.
+
+  \<^medskip> Automatic indentation has a tendency to produce trailing whitespace. That
+  can be purged manually with the jEdit action @{action "remove-trailing-ws"}
+  (shortcut \<^verbatim>\<open>C+e r\<close>). Moreover, the \<^emph>\<open>WhiteSpace\<close> plugin provides some
+  aggressive options to trim whitespace on buffer-save.
 \<close>