# HG changeset patch
# User wenzelm
# Date 1629742680 -7200
# Node ID 53e28c438f967ad967dfd5f032dd6b63fcd20bd9
# Parent  a3b0fc51070562cec2f01374df63910396fe606b
minor performance tuning;

diff -r a3b0fc510705 -r 53e28c438f96 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Mon Aug 23 14:24:57 2021 +0200
+++ b/src/Pure/General/symbol_pos.ML	Mon Aug 23 20:18:00 2021 +0200
@@ -40,7 +40,7 @@
   type text = string
   val implode: T list -> text
   val implode_range: Position.range -> T list -> text * Position.range
-  val explode_delete: text * Position.T -> T list * Position.T list
+  val explode_deleted: string * Position.T -> Position.T list
   val explode: text * Position.T -> T list
   val explode0: string -> T list
   val scan_ident: T list scanner
@@ -254,19 +254,25 @@
   let val syms' = (("", pos1) :: syms @ [("", pos2)])
   in (implode syms', range syms') end;
 
-fun explode_delete (str, pos) =
-  let
-    val (res, _) =
-      fold (fn s => fn (res, p) => ((s, p) :: res, Position.symbol s p))
-        (Symbol.explode str) ([], Position.no_range_position pos);
-  in
-    fold (fn (s, p) => if s = Symbol.DEL then apsnd (cons p) else apfst (cons (s, p)))
-      res ([], [])
-  end;
+local
+
+fun rev_explode (str, pos) =
+  fold (fn s => fn (res, p) => ((s, p) :: res, Position.symbol s p))
+    (Symbol.explode str) ([], Position.no_range_position pos)
+  |> #1;
+
+in
 
-val explode = explode_delete #> #1;
+fun explode_deleted arg =
+  fold (fn (s, p) => s = Symbol.DEL ? cons p) (rev_explode arg) [];
+
+fun explode arg =
+  fold (fn (s, p) => s <> Symbol.DEL ? cons (s, p)) (rev_explode arg) [];
+
 fun explode0 str = explode (str, Position.none);
 
+end;
+
 
 (* identifiers *)
 
diff -r a3b0fc510705 -r 53e28c438f96 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Mon Aug 23 14:24:57 2021 +0200
+++ b/src/Pure/Isar/token.ML	Mon Aug 23 20:18:00 2021 +0200
@@ -338,8 +338,8 @@
     let
       val pos = pos_of tok;
       val (m, text) = token_kind_markup (kind_of tok);
-      val delete = #2 (Symbol_Pos.explode_delete (source_of tok, pos));
-    in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) delete end;
+      val deleted = Symbol_Pos.explode_deleted (source_of tok, pos);
+    in ((pos, m), text) :: map (fn p => ((p, Markup.delete), "")) deleted end;
 
 fun markups keywords = map (#2 o #1) o reports keywords;