src/Pure/Tools/xml.ML
author wenzelm
Sat Jul 28 20:40:27 2007 +0200 (2007-07-28)
changeset 24022 ab76c73b3b58
parent 23784 75e6b9dd5336
permissions -rw-r--r--
tuned;
wenzelm@23614
     1
(*  Title:      Pure/Tools/xml.ML
wenzelm@23614
     2
    ID:         $Id$
wenzelm@23614
     3
    Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
wenzelm@23614
     4
wenzelm@23614
     5
Basic support for XML.
wenzelm@23614
     6
*)
wenzelm@23614
     7
wenzelm@23614
     8
signature XML =
wenzelm@23614
     9
sig
wenzelm@23614
    10
  (* string functions *)
wenzelm@23614
    11
  val header: string
wenzelm@23614
    12
  val text: string -> string
wenzelm@23614
    13
  val text_charref: string -> string
wenzelm@23614
    14
  val cdata: string -> string
wenzelm@23614
    15
  type attributes = (string * string) list
wenzelm@23632
    16
  val attribute: string * string -> string
wenzelm@23614
    17
  val element: string -> attributes -> string list -> string
wenzelm@23614
    18
  (* tree functions *)
wenzelm@23614
    19
  datatype tree =
wenzelm@23614
    20
      Elem of string * attributes * tree list
wenzelm@23723
    21
    | Text of string
wenzelm@23723
    22
    | Output of output
wenzelm@23614
    23
  type content = tree list
wenzelm@23614
    24
  type element = string * attributes * content
wenzelm@23614
    25
  val string_of_tree: tree -> string
wenzelm@23614
    26
  val buffer_of_tree: tree -> Buffer.T
wenzelm@23614
    27
  val parse_string : string -> string option
wenzelm@23614
    28
  val parse_content: string list -> tree list * string list
wenzelm@23614
    29
  val parse_elem: string list -> tree * string list
wenzelm@23614
    30
  val parse_document: string list -> (string option * tree) * string list
wenzelm@23614
    31
  val tree_of_string: string -> tree
wenzelm@23614
    32
  val scan_comment_whspc : string list -> unit * string list
wenzelm@23614
    33
end;
wenzelm@23614
    34
wenzelm@23614
    35
structure XML: XML =
wenzelm@23614
    36
struct
wenzelm@23614
    37
wenzelm@23614
    38
(** string based representation (small scale) **)
wenzelm@23614
    39
wenzelm@23614
    40
val header = "<?xml version=\"1.0\"?>\n";
wenzelm@23614
    41
wenzelm@23614
    42
wenzelm@23614
    43
(* text and character data *)
wenzelm@23614
    44
wenzelm@23614
    45
fun decode "&lt;" = "<"
wenzelm@23614
    46
  | decode "&gt;" = ">"
wenzelm@23614
    47
  | decode "&amp;" = "&"
wenzelm@23614
    48
  | decode "&apos;" = "'"
wenzelm@23614
    49
  | decode "&quot;" = "\""
wenzelm@23614
    50
  | decode c = c;
wenzelm@23614
    51
wenzelm@23614
    52
fun encode "<" = "&lt;"
wenzelm@23614
    53
  | encode ">" = "&gt;"
wenzelm@23614
    54
  | encode "&" = "&amp;"
wenzelm@23614
    55
  | encode "'" = "&apos;"
wenzelm@23614
    56
  | encode "\"" = "&quot;"
wenzelm@23614
    57
  | encode c = c;
wenzelm@23614
    58
wenzelm@23614
    59
fun encode_charref c = "&#" ^ Int.toString (ord c) ^ ";"
wenzelm@23614
    60
wenzelm@23614
    61
val text = Library.translate_string encode;
wenzelm@23614
    62
wenzelm@23614
    63
val text_charref = translate_string encode_charref;
wenzelm@23614
    64
wenzelm@23614
    65
val cdata = enclose "<![CDATA[" "]]>\n";
wenzelm@23614
    66
wenzelm@23614
    67
wenzelm@23614
    68
(* elements *)
wenzelm@23614
    69
wenzelm@23614
    70
fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\"";
wenzelm@23614
    71
wenzelm@23614
    72
fun element name atts cs =
wenzelm@23614
    73
  let val elem = space_implode " " (name :: map attribute atts) in
wenzelm@23614
    74
    if null cs then enclose "<" "/>" elem
wenzelm@23614
    75
    else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name
wenzelm@23614
    76
  end;
wenzelm@23614
    77
wenzelm@23614
    78
wenzelm@23614
    79
wenzelm@23614
    80
(** explicit XML trees **)
wenzelm@23614
    81
wenzelm@23614
    82
type attributes = (string * string) list;
wenzelm@23614
    83
wenzelm@23614
    84
datatype tree =
wenzelm@23614
    85
    Elem of string * attributes * tree list
wenzelm@23614
    86
  | Text of string
wenzelm@23723
    87
  | Output of output;
wenzelm@23614
    88
wenzelm@23614
    89
type content = tree list;
wenzelm@23614
    90
wenzelm@23614
    91
type element = string * attributes * content;
wenzelm@23614
    92
wenzelm@23614
    93
fun buffer_of_tree tree =
wenzelm@23614
    94
  let
wenzelm@23614
    95
    fun string_of (Elem (name, atts, ts)) buf =
wenzelm@23614
    96
        let val buf' =
wenzelm@23614
    97
          buf |> Buffer.add "<"
wenzelm@23614
    98
          |> fold Buffer.add (separate " " (name :: map attribute atts))
wenzelm@23614
    99
        in
wenzelm@23614
   100
          if null ts then
wenzelm@23614
   101
            buf' |> Buffer.add "/>"
wenzelm@23614
   102
          else
wenzelm@23614
   103
            buf' |> Buffer.add ">"
wenzelm@23614
   104
            |> fold string_of ts
wenzelm@23614
   105
            |> Buffer.add "</" |> Buffer.add name |> Buffer.add ">"
wenzelm@23614
   106
        end
wenzelm@23614
   107
      | string_of (Text s) buf = Buffer.add (text s) buf
wenzelm@23723
   108
      | string_of (Output s) buf = Buffer.add s buf;
wenzelm@23614
   109
  in string_of tree Buffer.empty end;
wenzelm@23614
   110
wenzelm@23614
   111
val string_of_tree = Buffer.content o buffer_of_tree;
wenzelm@23614
   112
wenzelm@23614
   113
wenzelm@23614
   114
wenzelm@23614
   115
(** XML parsing **)
wenzelm@23614
   116
wenzelm@23614
   117
fun err s (xs, _) =
wenzelm@23614
   118
  "XML parsing error: " ^ s ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);
wenzelm@23614
   119
wenzelm@23614
   120
val scan_whspc = Scan.many Symbol.is_blank;
wenzelm@23614
   121
wenzelm@23614
   122
val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
wenzelm@23614
   123
wenzelm@23614
   124
val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
wenzelm@23784
   125
  (scan_special || Scan.one Symbol.is_regular)) >> implode;
wenzelm@23614
   126
wenzelm@23614
   127
val parse_string = Scan.read Symbol.stopper parse_chars o explode;
wenzelm@23614
   128
wenzelm@23614
   129
val parse_cdata = Scan.this_string "<![CDATA[" |--
wenzelm@23784
   130
  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.is_regular)) >>
wenzelm@23614
   131
    implode) --| Scan.this_string "]]>";
wenzelm@23614
   132
wenzelm@23614
   133
val parse_att =
wenzelm@23614
   134
  Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
wenzelm@24022
   135
  (($$ "\"" || $$ "'") :|-- (fn s => (Scan.repeat (Scan.unless ($$ s)
wenzelm@24022
   136
    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s));
wenzelm@23614
   137
wenzelm@23614
   138
val parse_comment = Scan.this_string "<!--" --
wenzelm@23784
   139
  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --
wenzelm@23614
   140
  Scan.this_string "-->";
wenzelm@23614
   141
wenzelm@23614
   142
val scan_comment_whspc =
wenzelm@23614
   143
  (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
wenzelm@23614
   144
wenzelm@23614
   145
val parse_pi = Scan.this_string "<?" |--
wenzelm@23784
   146
  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.is_regular)) --|
wenzelm@23614
   147
  Scan.this_string "?>";
wenzelm@23614
   148
wenzelm@23614
   149
fun parse_content xs =
wenzelm@23614
   150
  ((Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) [] --
wenzelm@23614
   151
    (Scan.repeat ((* scan_whspc |-- *)
wenzelm@23614
   152
       (   parse_elem >> single
wenzelm@23614
   153
        || parse_cdata >> (single o Text)
wenzelm@23614
   154
        || parse_pi >> K []
wenzelm@23614
   155
        || parse_comment >> K []) --
wenzelm@23614
   156
       Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) []
wenzelm@23614
   157
         >> op @) >> flat) >> op @)(* --| scan_whspc*)) xs
wenzelm@23614
   158
wenzelm@23614
   159
and parse_elem xs =
wenzelm@23614
   160
  ($$ "<" |-- Symbol.scan_id --
wenzelm@23614
   161
    Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
wenzelm@23614
   162
      !! (err "Expected > or />")
wenzelm@23614
   163
        (Scan.this_string "/>" >> K []
wenzelm@23614
   164
         || $$ ">" |-- parse_content --|
wenzelm@23614
   165
            !! (err ("Expected </" ^ s ^ ">"))
wenzelm@23614
   166
              (Scan.this_string ("</" ^ s) --| scan_whspc --| $$ ">"))) >>
wenzelm@23614
   167
    (fn ((s, atts), ts) => Elem (s, atts, ts))) xs;
wenzelm@23614
   168
wenzelm@23614
   169
val parse_document =
wenzelm@23614
   170
  Scan.option (Scan.this_string "<!DOCTYPE" -- scan_whspc |--
wenzelm@23614
   171
    (Scan.repeat (Scan.unless ($$ ">")
wenzelm@23784
   172
      (Scan.one Symbol.is_regular)) >> implode) --| $$ ">" --| scan_whspc) --
wenzelm@23614
   173
  parse_elem;
wenzelm@23614
   174
wenzelm@23614
   175
fun tree_of_string s =
wenzelm@23614
   176
  (case Scan.finite Symbol.stopper (Scan.error (!! (err "Malformed element")
wenzelm@23614
   177
      (scan_whspc |-- parse_elem --| scan_whspc))) (Symbol.explode s) of
wenzelm@23614
   178
    (x, []) => x
wenzelm@23614
   179
  | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
wenzelm@23614
   180
wenzelm@23614
   181
end;