Revert change to pgml_sym
authoraspinall
Wed Oct 27 19:45:16 2004 +0200 (2004-10-27)
changeset 152660398af5501fe
parent 15265 a1547232fedd
child 15267 96c59666a0bf
Revert change to pgml_sym
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Wed Oct 27 10:30:07 2004 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Wed Oct 27 19:45:16 2004 +0200
     1.3 @@ -89,8 +89,10 @@
     1.4    (case Symbol.decode s of
     1.5      (* NB: an alternative here would be to output the default print mode alternative
     1.6         in the element content, but unfortunately print modes are not that fine grained. *)
     1.7 -    Symbol.Sym s => XML.element "sym" [("name", s)] [XML.text s]
     1.8 -  | _ => XML.text s)
     1.9 +    Symbol.Char s => XML.text s
    1.10 +  | Symbol.Sym s => XML.element "sym" [("name", s)] [XML.text s]
    1.11 +  | Symbol.Ctrl s => XML.element "ctrl" [("name", s)] []  (* FIXME: no such PGML! *)
    1.12 +  | Symbol.Raw s => s);
    1.13  
    1.14  fun pgml_output str =
    1.15    let val syms = Symbol.explode str