--- 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 {