support for javax.swing.JLabel.labelFor following the Java Swing Tutorial on Assistive Technologies, although it has no immediate impact on NVDA;

--- a/src/Pure/GUI/gui.scala	Thu Aug 21 12:39:08 2025 +0200
+++ b/src/Pure/GUI/gui.scala	Thu Aug 21 19:55:30 2025 +0200
@@ -12,10 +12,11 @@
 import java.awt.event.{KeyAdapter, KeyEvent}
 import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute}
 import java.awt.geom.AffineTransform
-import javax.swing.{ImageIcon, JButton, JLabel, JLayeredPane, JOptionPane,
+import javax.swing.{Icon, ImageIcon, JButton, JLabel, JLayeredPane, JOptionPane,
   RootPaneContainer, JTextField, JComboBox, LookAndFeel, UIManager, SwingUtilities}
 
-import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Separator}
+import scala.swing.{Alignment, CheckBox, ComboBox, ScrollPane, TextArea, ListView, Separator}
+import scala.swing.Swing.EmptyIcon
 import scala.swing.event.{ButtonClicked, SelectionChanged}
 
 import com.formdev.flatlaf
@@ -228,6 +229,33 @@
   }
 
 
+  /* label for other component */
+
+  class Label(
+    label_text: String,
+    label_icon: Icon,
+    label_align: Alignment.Value,
+    label_for: java.awt.Component
+  ) extends scala.swing.Label(label_text, label_icon, label_align) {
+
+    override lazy val peer: JLabel =
+      new JLabel(label_text, if (label_icon == EmptyIcon) null else label_icon, label_align.id)
+        with SuperMixin { labelFor = label_for }
+
+    override def this(label_text: String, label_icon: Icon, label_align: Alignment.Value) =
+      this(label_text, label_icon, label_align, null)
+
+    def this(label_text: String, label_for: java.awt.Component) =
+      this(label_text, EmptyIcon, Alignment.Center, label_for)
+
+    def this(label_text: String, label_for: scala.swing.Component) =
+      this(label_text, EmptyIcon, Alignment.Center, label_for.peer)
+
+    def this(label_text: String) =
+      this(label_text, EmptyIcon, Alignment.Center)
+  }
+
+
   /* list selector */
 
   object Selector {

--- a/src/Tools/Graphview/tree_panel.scala	Thu Aug 21 12:39:08 2025 +0200
+++ b/src/Tools/Graphview/tree_panel.scala	Thu Aug 21 19:55:30 2025 +0200
@@ -91,14 +91,11 @@
       case Some(re) => re.findFirstIn(node.toString).isDefined
     }
 
-  private val selection_label = new Label("Selection:") {
-    tooltip = "Selection of nodes via regular expression"
-  }
-
-  private val selection_field = new TextField(10) {
-    tooltip = selection_label.tooltip
-  }
+  private val selection_tooltip = "Selection of nodes via regular expression"
+  private val selection_field = new TextField(10) { tooltip = selection_tooltip }
   private val selection_field_foreground = selection_field.foreground
+  private val selection_label =
+    new GUI.Label("Selection:", selection_field) { tooltip = selection_tooltip }
 
   private val selection_delay =
     Delay.last(graphview.options.seconds("editor_input_delay"), gui = true) {

--- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Aug 21 12:39:08 2025 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Thu Aug 21 19:55:30 2025 +0200
@@ -15,7 +15,7 @@
 import javax.swing.event.TreeSelectionEvent
 
 import scala.collection.immutable.SortedMap
-import scala.swing.{Label, Component}
+import scala.swing.Component
 
 import org.gjt.sp.jedit.{jEdit, View}
 import org.gjt.sp.jedit.menu.EnhancedMenuItem
@@ -182,9 +182,7 @@
     override def clicked(): Unit = thread_selection().foreach(debugger.step_out)
   }
 
-  private val context_label = new Label("Context:") {
-    tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic"
-  }
+  private val context_tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic"
   private val context_field =
     new Completion_Popup.History_Text_Field("isabelle-debugger-context") {
       override def processKeyEvent(evt: KeyEvent): Unit = {
@@ -194,13 +192,14 @@
         super.processKeyEvent(evt)
       }
       setColumns(20)
-      setToolTipText(context_label.tooltip)
+      setToolTipText(context_tooltip)
       setFont(GUI.imitate_font(getFont, scale = 1.2))
     }
+  private val context_label = new GUI.Label("Context:", context_field) {
+    tooltip = context_tooltip
+  }
 
-  private val expression_label = new Label("ML:") {
-    tooltip = "Isabelle/ML or Standard ML expression"
-  }
+  private val expression_tooltip = "Isabelle/ML or Standard ML expression"
   private val expression_field =
     new Completion_Popup.History_Text_Field("isabelle-debugger-expression") {
       override def processKeyEvent(evt: KeyEvent): Unit = {
@@ -211,9 +210,12 @@
       }
       { val max = getPreferredSize; max.width = Int.MaxValue; setMaximumSize(max) }
       setColumns(40)
-      setToolTipText(expression_label.tooltip)
+      setToolTipText(expression_tooltip)
       setFont(GUI.imitate_font(getFont, scale = 1.2))
     }
+  private val expression_label = new GUI.Label("ML:", expression_field) {
+    tooltip = expression_tooltip
+  }
 
   private val eval_button =
     new GUI.Button(GUI.Style_HTML.enclose_bold("Eval")) {

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Aug 21 12:39:08 2025 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Aug 21 19:55:30 2025 +0200
@@ -16,7 +16,7 @@
 import javax.swing.JTextField
 import javax.swing.event.{DocumentListener, DocumentEvent}
 
-import scala.swing.{Label, Component}
+import scala.swing.Component
 import scala.util.matching.Regex
 
 import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction}
@@ -266,9 +266,7 @@
 
   /* search */
 
-  private val search_label: Component = new Label(jEdit.getProperty("view.search.find")) {
-    tooltip = "Search and highlight output via regular expression"
-  }
+  private val search_tooltip = "Search and highlight output via regular expression"
 
   private val search_field: Component =
     Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search") {
@@ -280,12 +278,17 @@
         def removeUpdate(e: DocumentEvent): Unit = input_delay.invoke()
       })
       setColumns(20)
-      setToolTipText(search_label.tooltip)
+      setToolTipText(search_tooltip)
       setFont(GUI.imitate_font(getFont, scale = 1.2))
     })
 
   private val search_field_foreground = search_field.foreground
 
+  private val search_label: Component =
+    new GUI.Label(jEdit.getProperty("view.search.find"), label_for = search_field) {
+      tooltip = search_tooltip
+    }
+
   private def search_action(text_field: JTextField): Unit = {
     val (pattern, ok) =
       text_field.getText match {

--- a/src/Tools/jEdit/src/query_dockable.scala	Thu Aug 21 12:39:08 2025 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Thu Aug 21 19:55:30 2025 +0200
@@ -84,14 +84,15 @@
       query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
     }
 
-    private val query_label = new Label("Find:") {
-      tooltip =
-        GUI.tooltip_lines(
-          "Search criteria for find operation, e.g.\n\"_ = _\" \"(+)\" name: Group -name: monoid")
-    }
+    private val query_tooltip =
+      GUI.tooltip_lines(
+        "Search criteria for find operation, e.g.\n\"_ = _\" \"(+)\" name: Group -name: monoid")
 
     val query: Completion_Popup.History_Text_Field =
-      make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
+      make_query("isabelle-find-theorems", query_tooltip, apply_query _)
+
+    private val query_label =
+      new GUI.Label("Find:", query) { tooltip = query_tooltip }
 
 
     /* GUI page */

--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu Aug 21 12:39:08 2025 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu Aug 21 19:55:30 2025 +0200
@@ -63,21 +63,20 @@
       List(provers.getText, isar_proofs.selected.toString, try0.selected.toString))
   }
 
-  private val provers_label = new Label("Provers:") {
-    tooltip =
-      GUI.tooltip_lines(
-        "Automatic provers as space-separated list, e.g.\n" +
-          PIDE.options.value.check_name("sledgehammer_provers").default_value)
-  }
-
+  private val provers_tooltip =
+    GUI.tooltip_lines(
+      "Automatic provers as space-separated list, e.g.\n" +
+        PIDE.options.value.check_name("sledgehammer_provers").default_value)
   private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
     override def processKeyEvent(evt: KeyEvent): Unit = {
       if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) hammer()
       super.processKeyEvent(evt)
     }
-    setToolTipText(provers_label.tooltip)
+    setToolTipText(provers_tooltip)
     setColumns(30)
   }
+  private val provers_label =
+    new GUI.Label("Provers:", provers) { tooltip = provers_tooltip }
 
   private def update_provers(): Unit = {
     val new_provers = PIDE.options.string("sledgehammer_provers")

--- a/src/Tools/jEdit/src/timing_dockable.scala	Thu Aug 21 12:39:08 2025 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Thu Aug 21 19:55:30 2025 +0200
@@ -109,11 +109,6 @@
   private var timing_threshold = PIDE.options.real("jedit_timing_threshold")
 
   private val threshold_tooltip = "Threshold for timing display (seconds)"
-
-  private val threshold_label = new Label("Threshold: ") {
-    tooltip = threshold_tooltip
-  }
-
   private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {
     reactions += {
       case _: ValueChanged =>
@@ -126,6 +121,8 @@
     tooltip = threshold_tooltip
     verifier = { case Value.Double(x) => x >= 0.0 case _ => false }
   }
+  private val threshold_label =
+    new GUI.Label("Threshold: ", threshold_value) { tooltip = threshold_tooltip }
 
   private val controls = Wrap_Panel(List(threshold_label, threshold_value))