# HG changeset patch
# User aspinall
# Date 1096361059 -7200
# Node ID 4ff917a91e1618a1bcd569260099b0521bea9a20
# Parent  b62f72ea3bb031cdcbac81af258cc320ea751b36
Remove double escaping of backslash in PGML.  Remove use of character refs in <whitespace>

diff -r b62f72ea3bb0 -r 4ff917a91e16 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Tue Sep 28 10:43:34 2004 +0200
+++ b/src/Pure/proof_general.ML	Tue Sep 28 10:44:19 2004 +0200
@@ -87,8 +87,7 @@
 
 fun pgml_sym s =
   (case Symbol.decode s of
-    Symbol.Char "\\" => "\\\\"
-  | Symbol.Char s => XML.text s
+    Symbol.Char s => XML.text s
   | Symbol.Sym s => XML.element "sym" [("name", s)] []
   | Symbol.Ctrl s => XML.element "ctrl" [("name", s)] []
   | Symbol.Raw s => s);
@@ -736,10 +735,7 @@
     fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]]
     fun empty elt = [XML.element elt [] []]
 
-    fun whitespace "" = ""
-      | whitespace str = XML.element "whitespace" []
-				(map (fn c=> "&#"^Int.toString (Char.ord c)^ ";") 
-				     (String.explode str))
+    fun whitespace str = XML.element "whitespace" [] [XML.text str]
 
     (* an extra token is needed to terminate the command *)
     val sync = OuterSyntax.scan "\\<^sync>";
@@ -923,7 +919,7 @@
 	val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
     in 
 	if (prewhs <> []) then
-	    whitespace (implode (map OuterLex.unparse prewhs)) 
+	    whitespace (implode (map OuterLex.unparse prewhs))
 	    :: (markup_comment_whs rest)
 	else 
 	    (markup_text (OuterLex.unparse t) "comment") @