Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
- tuned text function
authorberghofe
Fri, 16 Apr 2004 18:43:36 +0200
changeset 14596 c36e116b578b
parent 14595 2df717e26035
child 14597 ee0fb03f5f1e
- tuned text function - Replaced quote by Library.quote, since quote now refers to Symbol.quote
src/Pure/General/xml.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle