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