# HG changeset patch
# User berghofe
# Date 1082133816 -7200
# Node ID c36e116b578b770ccaf7d1525303b804b1a2c81a
# Parent  2df717e26035faad88f2543ce5058d550c2cc947
- tuned text function
- Replaced quote by Library.quote, since quote now refers to Symbol.quote

diff -r 2df717e26035 -r c36e116b578b src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Fri Apr 16 18:42:02 2004 +0200
+++ b/src/Pure/General/xml.ML	Fri Apr 16 18:43:36 2004 +0200
@@ -41,7 +41,7 @@
   | decode """ = "\""
   | decode c = c;
 
-val text = implode o map encode o explode;
+val text = String.translate (encode o String.str);
 
 
 (* elements *)
@@ -50,7 +50,7 @@
     Elem of string * (string * string) list * tree list
   | Text of string;
 
-fun attribute (a, x) = a ^ " = " ^ quote (text x);
+fun attribute (a, x) = a ^ " = " ^ Library.quote (text x);
 
 fun element name atts cs =
   let val elem = space_implode " " (name :: map attribute atts) in