Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more uniform tooltip for plugin options dialog;
authorwenzelm
Tue, 06 Dec 2022 16:42:08 +0100
changeset 76581 e5bf43eda6ed
parent 76580 699d9a219e45
child 76582 71942a6af4ed
more uniform tooltip for plugin options dialog;
src/Tools/jEdit/src/jedit_sessions.scala file | annotate | diff | comparison | revisions 
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Dec 06 16:38:50 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Dec 06 16:42:08 2022 +0100
@@ -76,7 +76,9 @@
     batches: List[GUI.Selector.Entry[String]]*)
   extends GUI.Selector[String](batches: _*) with JEdit_Options.Entry {
     name = option_name
-    tooltip = Word.capitalize(options.value.description(option_name))
+    tooltip =
+      if (standalone) Word.capitalize(options.value.description(option_name))
+      else options.value.check_name(option_name).print_default
 
     override val title: String =
       options.value.check_name(option_name).title_jedit
isabelle