more uniform treatment of threshold for command timings;

--- a/NEWS	Tue Sep 16 13:52:24 2025 +0200
+++ b/NEWS	Tue Sep 16 14:19:34 2025 +0200
@@ -408,6 +408,11 @@
 information later on, using Thy_Info.get_theory_segments or
 Thy_Info.get_theory_elements in Isabelle/ML.
 
+* System option "command_timing_threshold" has been renamed to
+"build_timing_threshold": it refers to batch-builds. Likewise,
+"jedit_timing_threshold" and "vscode_timing_threshold" have been unified
+as "editor_timing_threshold": it refers to PIDE editor interaction.
+
 * The Z Garbage Collector (ZGC) of Java 21 is now used by default (see
 also https://wiki.openjdk.org/display/zgc). This should work uniformly
 on all platforms, but requires a reasonably new version of Windows

--- a/etc/options	Tue Sep 16 13:52:24 2025 +0200
+++ b/etc/options	Tue Sep 16 14:19:34 2025 +0200
@@ -107,8 +107,8 @@
 option parallel_subproofs_threshold : real = 0.01 for build
   -- "lower bound of timing estimate for forked nested proofs (seconds)"
 
-option command_timing_threshold : real = 0.1 for build
-  -- "default threshold for persistent command timing (seconds)"
+option build_timing_threshold : real = 0.1 for build
+  -- "threshold for persistent storage of command timings (seconds)"
 
 public option timeout_scale : real = 1.0 for build
   -- "scale factor for timeout in Isabelle/ML and session build"
@@ -344,6 +344,9 @@
 option editor_syslog_limit : int = 100
   -- "maximum amount of buffered syslog messages"
 
+public option editor_timing_threshold : real = 0.1
+  -- "threshold for interactive display of command timings (seconds)"
+
 
 section "Headless Session"
 

--- a/src/Pure/Build/build_job.scala	Tue Sep 16 13:52:24 2025 +0200
+++ b/src/Pure/Build/build_job.scala	Tue Sep 16 14:19:34 2025 +0200
@@ -281,7 +281,7 @@
                 elapsed <- Markup.Elapsed.unapply(props)
                 elapsed_time = Time.seconds(elapsed)
                 if elapsed_time.is_relevant &&
-                   elapsed_time >= options.seconds("command_timing_threshold")
+                   elapsed_time >= options.seconds("build_timing_threshold")
               } command_timings += props.filter(Markup.command_timing_property)
           }
 

--- a/src/Pure/PIDE/rendering.scala	Tue Sep 16 13:52:24 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala	Tue Sep 16 14:19:34 2025 +0200
@@ -617,7 +617,7 @@
 
   /* tooltips */
 
-  def timing_threshold: Double = 0.0
+  def timing_threshold: Double = options.real("editor_timing_threshold")
 
   private sealed case class Tooltip_Info(
     range: Text.Range,
@@ -645,7 +645,7 @@
 
     def timing_info(elem: XML.Elem): Option[XML.Elem] =
       if (elem.markup.name == Markup.TIMING) {
-        if (timing.elapsed.seconds >= timing_threshold) {
+        if (timing.is_relevant && timing.elapsed.seconds >= timing_threshold) {
           Some(Pretty.string(timing.message))
         }
         else None

--- a/src/Tools/VSCode/etc/options	Tue Sep 16 13:52:24 2025 +0200
+++ b/src/Tools/VSCode/etc/options	Tue Sep 16 14:19:34 2025 +0200
@@ -15,9 +15,6 @@
 option vscode_message_margin : int = 80 for vscode
   -- "margin for pretty-printing of diagnostic messages"
 
-option vscode_timing_threshold : real = 0.1 for vscode
-  -- "default threshold for timing display (seconds)"
-
 option vscode_pide_extensions : bool = false for vscode
   -- "use PIDE extensions for Language Server Protocol"
 

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Sep 16 13:52:24 2025 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Sep 16 14:19:34 2025 +0200
@@ -251,11 +251,6 @@
   }
 
 
-  /* tooltips */
-
-  override def timing_threshold: Double = options.real("vscode_timing_threshold")
-
-
   /* hyperlinks */
 
   def hyperlink_source_file(

--- a/src/Tools/jEdit/etc/options	Tue Sep 16 13:52:24 2025 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Sep 16 14:19:34 2025 +0200
@@ -33,9 +33,6 @@
 public option jedit_symbols_search_limit : int = 50
   -- "maximum number of symbols in search result"
 
-public option jedit_timing_threshold : real = 0.1
-  -- "default threshold for timing display (seconds)"
-
 public option jedit_text_overview : bool = true
   -- "paint text overview column"
 

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Sep 16 13:52:24 2025 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Sep 16 14:19:34 2025 +0200
@@ -310,7 +310,6 @@
   /* tooltips */
 
   def tooltip_margin: Int = options.int("jedit_tooltip_margin")
-  override def timing_threshold: Double = options.real("jedit_timing_threshold")
 
   def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[List[XML.Elem]]] =
     tooltips(if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements,

--- a/src/Tools/jEdit/src/timing_dockable.scala	Tue Sep 16 13:52:24 2025 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala	Tue Sep 16 14:19:34 2025 +0200
@@ -106,7 +106,7 @@
 
   /* timing threshold */
 
-  private var timing_threshold = PIDE.options.real("jedit_timing_threshold")
+  private var timing_threshold = PIDE.options.real("editor_timing_threshold")
 
   private val threshold_tooltip = "Threshold for timing display (seconds)"
   private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {