--- a/src/Pure/PIDE/yxml.ML Fri Jul 05 00:18:51 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML Fri Jul 05 00:21:47 2024 +0200
@@ -18,7 +18,6 @@
sig
val X: Symbol.symbol
val Y: Symbol.symbol
- val embed_controls: string -> string
val detect: string -> bool
val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
val tree_size: XML.tree -> int
@@ -41,19 +40,6 @@
(** string representation **)
-(* idempotent recoding of certain low ASCII control characters *)
-
-fun pseudo_utf8 c =
- if Symbol.is_ascii_control c
- then chr 192 ^ chr (128 + ord c)
- else c;
-
-fun embed_controls str =
- if exists_string Symbol.is_ascii_control str
- then translate_string pseudo_utf8 str
- else str;
-
-
(* markers *)
val X_char = Char.chr 5;