# HG changeset patch
# User wenzelm
# Date 1726061774 -7200
# Node ID a34eca8caccb79e0cc7e7f6b32ea33bbd05353ed
# Parent  7560e1a69680d569d2c04edb78dd6ea744cc0b82
minor performance tuning, notably for Bytes.add (e.g. YXML output);

diff -r 7560e1a69680 -r a34eca8caccb src/Pure/ML/ml_init.ML
--- a/src/Pure/ML/ml_init.ML	Wed Sep 11 12:46:56 2024 +0200
+++ b/src/Pure/ML/ml_init.ML	Wed Sep 11 15:36:14 2024 +0200
@@ -34,4 +34,15 @@
 struct
   open Substring;
   val empty = full "";
+
+local
+  val chars = Vector.tabulate (Char.maxOrd, Substring.full o String.str o Char.chr);
+in
+  fun full str =
+    (case String.size str of
+      0 => empty
+    | 1 => Vector.sub (chars, Char.ord (String.sub (str, 0)))
+    | _ => Substring.full str);
 end;
+
+end;