# HG changeset patch
# User wenzelm
# Date 1726742462 -7200
# Node ID f4d519d088afb745efe6fb69eba8c8b643d8058f
# Parent  2c75875ccf94641a33717d0c10b4f1dd53f59ad0
minor performance tuning: avoid vacuous update of context;

diff -r 2c75875ccf94 -r f4d519d088af src/Pure/config.ML
--- a/src/Pure/config.ML	Thu Sep 19 12:10:17 2024 +0200
+++ b/src/Pure/config.ML	Thu Sep 19 12:41:02 2024 +0200
@@ -7,6 +7,7 @@
 signature CONFIG =
 sig
   datatype value = Bool of bool | Int of int | Real of real | String of string
+  val eq_value: value * value -> bool
   val print_value: value -> string
   val print_type: value -> string
   type 'a T
@@ -58,6 +59,12 @@
   Real of real |
   String of string;
 
+fun eq_value (Bool a, Bool b) = a = b
+  | eq_value (Int a, Int b) = a = b
+  | eq_value (Real a, Real b) = eq_real (a, b)
+  | eq_value (String a, String b) = a = b
+  | eq_value _ = false;
+
 fun print_value (Bool true) = "true"
   | print_value (Bool false) = "false"
   | print_value (Int i) = Value.print_int i
@@ -143,13 +150,23 @@
   let
     val id = serial ();
 
+    val lookup_value = Inttab.lookup o Data.get;
+
+    fun the_default_value _ (SOME value) = value
+      | the_default_value context NONE = default context;
+
     fun get_value context =
-      (case Inttab.lookup (Data.get context) id of
-        SOME value => value
-      | NONE => default context);
+      the_default_value context (lookup_value context id);
 
     fun map_value f context =
-      Data.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context;
+      let
+        val old = lookup_value context id;
+        val old_value = the_default_value context old;
+        val new_value = type_check (name, pos) f old_value;
+      in
+        if eq_option eq_value (old, SOME new_value) then context
+        else Data.map (Inttab.update (id, new_value)) context
+      end;
   in
     Config {name = name, pos = pos, get_value = get_value, map_value = map_value}
   end;