src/Pure/General/xml.ML
author wenzelm
Fri Dec 14 11:52:54 2001 +0100 (2001-12-14)
changeset 12498 3b0091bf06e8
parent 12416 9b3e7a35da30
child 13729 1a8dda49fd86
permissions -rw-r--r--
changed Thm.varifyT';
     1 (*  Title:      Pure/General/xml.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, LMU München
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Basic support for XML output.
     7 *)
     8 
     9 signature XML =
    10 sig
    11   val element: string -> (string * string) list -> string list -> string
    12   val text: string -> string
    13   val header: string
    14 end;
    15 
    16 structure XML: XML =
    17 struct
    18 
    19 (* character data *)
    20 
    21 fun encode "<" = "&lt;"
    22   | encode ">" = "&gt;"
    23   | encode "&" = "&amp;"
    24   | encode "'" = "&apos;"
    25   | encode "\"" = "&quot;"
    26   | encode c = c;
    27 
    28 val text = implode o map encode o explode;
    29 
    30 
    31 (* elements *)
    32 
    33 fun attribute (a, x) = a ^ " = " ^ quote (text x);
    34 
    35 fun element name atts cs =
    36   let val elem = space_implode " " (name :: map attribute atts) in
    37     if null cs then enclose "<" "/>" elem
    38     else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name
    39   end;
    40 
    41 val header = "<?xml version=\"1.0\"?>\n";
    42 
    43 end;