# HG changeset patch
# User wenzelm
# Date 1675092370 -3600
# Node ID 61f6bb753cbf5c0c0fa60465238299023b55552a
# Parent  139a0119ae3c0e6393d372719b3017dceec3db66
more operations;

diff -r 139a0119ae3c -r 61f6bb753cbf src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Mon Jan 30 16:20:17 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala	Mon Jan 30 16:26:10 2023 +0100
@@ -23,6 +23,7 @@
   /* typed access and GUI components */
 
   class Access[A](access: Options.Access_Variable[A], val name: String) {
+    def description: String = access.options.value.description(name)
     def apply(): A = access.apply(name)
     def update(x: A): Unit = change(_ => x)
     def change(f: A => A): Unit = {
@@ -73,6 +74,7 @@
   }
 
 
+
   /* editor pane for plugin options */
 
   trait Entry extends Component {