Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
authoraspinall
Tue Sep 28 10:44:19 2004 +0200 (2004-09-28)
changeset 152104ff917a91e16
parent 15209 b62f72ea3bb0
child 15211 5f54721547a7
Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Tue Sep 28 10:43:34 2004 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Tue Sep 28 10:44:19 2004 +0200
     1.3 @@ -87,8 +87,7 @@
     1.4  
     1.5  fun pgml_sym s =
     1.6    (case Symbol.decode s of
     1.7 -    Symbol.Char "\\" => "\\\\"
     1.8 -  | Symbol.Char s => XML.text s
     1.9 +    Symbol.Char s => XML.text s
    1.10    | Symbol.Sym s => XML.element "sym" [("name", s)] []
    1.11    | Symbol.Ctrl s => XML.element "ctrl" [("name", s)] []
    1.12    | Symbol.Raw s => s);
    1.13 @@ -736,10 +735,7 @@
    1.14      fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]]
    1.15      fun empty elt = [XML.element elt [] []]
    1.16  
    1.17 -    fun whitespace "" = ""
    1.18 -      | whitespace str = XML.element "whitespace" []
    1.19 -				(map (fn c=> "&#"^Int.toString (Char.ord c)^ ";") 
    1.20 -				     (String.explode str))
    1.21 +    fun whitespace str = XML.element "whitespace" [] [XML.text str]
    1.22  
    1.23      (* an extra token is needed to terminate the command *)
    1.24      val sync = OuterSyntax.scan "\\<^sync>";
    1.25 @@ -923,7 +919,7 @@
    1.26  	val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
    1.27      in 
    1.28  	if (prewhs <> []) then
    1.29 -	    whitespace (implode (map OuterLex.unparse prewhs)) 
    1.30 +	    whitespace (implode (map OuterLex.unparse prewhs))
    1.31  	    :: (markup_comment_whs rest)
    1.32  	else 
    1.33  	    (markup_text (OuterLex.unparse t) "comment") @