# HG changeset patch
# User wenzelm
# Date 1397332738 -7200
# Node ID 7bef3cd6a69ce4ccd2d57b9f7d288f49173d4f36
# Parent  f56dfc30e4b6f4838d47d1bf06e19b2270b32967
NEWS;

diff -r f56dfc30e4b6 -r 7bef3cd6a69c NEWS
--- a/NEWS	Sat Apr 12 21:44:38 2014 +0200
+++ b/NEWS	Sat Apr 12 21:58:58 2014 +0200
@@ -94,6 +94,8 @@
   - More reliable treatment of GUI events vs. completion popups: avoid
     loosing keystrokes with slow / remote graphics displays.
 
+* Spell-checker support for document text, comments etc.
+
 * Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
 Open text buffers take precedence over copies within the file-system.
 
diff -r f56dfc30e4b6 -r 7bef3cd6a69c src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sat Apr 12 21:44:38 2014 +0200
+++ b/src/Tools/jEdit/etc/options	Sat Apr 12 21:58:58 2014 +0200
@@ -52,7 +52,7 @@
 section "Spell Checker"
 
 public option spell_checker : bool = true
-  -- "enable spell-checker for prose words within document text"
+  -- "enable spell-checker for prose words within document text, comments etc."
 
 public option spell_checker_language : string = "en"
   -- "language for spell-checker locale and dictionary (en, de, fr)"