diff -r d0d0953e063f -r ac74eedb910a src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Mon Jan 05 11:15:30 2015 +0100
+++ b/src/Tools/jEdit/etc/options	Mon Jan 05 14:13:38 2015 +0100
@@ -10,13 +10,13 @@
   -- "load all required files automatically to resolve theory imports"
 
 public option jedit_reset_font_size : int = 18
-  -- "reset font size for main text area"
+  -- "reset main text font size"
 
 public option jedit_font_scale : real = 1.0
-  -- "scale factor of add-on panels wrt. main text area"
+  -- "scale factor of add-on panels wrt. main text font"
 
 public option jedit_popup_font_scale : real = 0.85
-  -- "scale factor of popups wrt. main text area"
+  -- "scale factor of popups wrt. main text font"
 
 public option jedit_popup_bounds : real = 0.5
   -- "relative bounds of popup window wrt. logical screen size"