src/Tools/jEdit/src/jedit_options.scala

--- a/src/Tools/jEdit/src/jedit_options.scala	Fri May 17 23:31:02 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Sat May 18 12:41:31 2013 +0200
@@ -25,6 +25,11 @@
   def save(): Unit
 }
 
+object JEdit_Options
+{
+  val RENDERING_SECTION = "Rendering of Document Content"
+}
+
 class JEdit_Options extends Options_Variable
 {
   def color_value(s: String): Color = Color_Value(string(s))