# HG changeset patch
# User wenzelm
# Date 1730990555 -3600
# Node ID 71e66ebbc6323bb35d39b23ec95823a5487b93a1
# Parent  5c8c94d5211a3347393d4c476c05b156b5347ce4
tuned: fewer warnings in IntelliJ IDEA;

diff -r 5c8c94d5211a -r 71e66ebbc632 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 07 13:30:40 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 07 15:42:35 2024 +0100
@@ -145,11 +145,11 @@
 
   /* search */
 
-  val search_label: Component = new Label("Search:") {
+  private val search_label: Component = new Label("Search:") {
     tooltip = "Search and highlight output via regular expression"
   }
 
-  val search_field: Component =
+  private val search_field: Component =
     Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search") {
       private val input_delay =
         Delay.last(PIDE.session.input_delay, gui = true) { search_action(this) }
@@ -224,7 +224,7 @@
 
         case KeyEvent.VK_A
         if strict_control =>
-          text_area.selectAll
+          text_area.selectAll()
           evt.consume()
 
         case KeyEvent.VK_ESCAPE =>