src/HOL/Import/xml.ML
author wenzelm
Thu May 27 18:10:37 2010 +0200 (2010-05-27)
changeset 37146 f652333bbf8e
parent 32960 69916a850301
child 41491 a2ad5b824051
permissions -rw-r--r--
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
haftmann@24584
     1
(*  Title:      HOL/Import/xml.ML
obua@19064
     2
wenzelm@26537
     3
Yet another version of XML support.
obua@19064
     4
*)
obua@19064
     5
obua@19064
     6
signature XML =
obua@19064
     7
sig
obua@19064
     8
  val header: string
obua@19064
     9
  val text: string -> string
obua@19064
    10
  val text_charref: string -> string
obua@19064
    11
  val cdata: string -> string
obua@19064
    12
  val element: string -> (string * string) list -> string list -> string
obua@19089
    13
  
obua@19064
    14
  datatype tree =
obua@19064
    15
      Elem of string * (string * string) list * tree list
obua@19064
    16
    | Text of string
obua@19089
    17
  
obua@19064
    18
  val string_of_tree: tree -> string
obua@19064
    19
  val tree_of_string: string -> tree
obua@19089
    20
obua@19089
    21
  val encoded_string_of_tree : tree -> string
obua@19089
    22
  val tree_of_encoded_string : string -> tree
obua@19064
    23
end;
obua@19064
    24
obua@19089
    25
structure XML :> XML =
obua@19064
    26
struct
obua@19064
    27
obua@19093
    28
(*structure Seq = VectorScannerSeq
obua@19093
    29
structure Scan = Scanner (structure Seq = Seq)*)
obua@19093
    30
structure Seq = StringScannerSeq
obua@19093
    31
structure Scan = StringScanner
obua@19093
    32
obua@19095
    33
obua@19064
    34
open Scan
obua@19064
    35
obua@19064
    36
(** string based representation (small scale) **)
obua@19064
    37
obua@19064
    38
val header = "<?xml version=\"1.0\"?>\n";
obua@19064
    39
obua@19064
    40
(* text and character data *)
obua@19064
    41
obua@19064
    42
fun decode "&lt;" = "<"
obua@19064
    43
  | decode "&gt;" = ">"
obua@19064
    44
  | decode "&amp;" = "&"
obua@19064
    45
  | decode "&apos;" = "'"
obua@19064
    46
  | decode "&quot;" = "\""
obua@19064
    47
  | decode c = c;
obua@19064
    48
obua@19064
    49
fun encode "<" = "&lt;"
obua@19064
    50
  | encode ">" = "&gt;"
obua@19064
    51
  | encode "&" = "&amp;"
obua@19064
    52
  | encode "'" = "&apos;"
obua@19064
    53
  | encode "\"" = "&quot;"
obua@19064
    54
  | encode c = c;
obua@19064
    55
obua@19064
    56
fun encode_charref c = "&#" ^ Int.toString (ord c) ^ ";"
obua@19064
    57
obua@19064
    58
val text = Library.translate_string encode
obua@19064
    59
obua@19064
    60
val text_charref = translate_string encode_charref;
obua@19064
    61
obua@19064
    62
val cdata = enclose "<![CDATA[" "]]>\n"
obua@19064
    63
obua@19064
    64
(* elements *)
obua@19064
    65
obua@19064
    66
fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\"";
obua@19064
    67
obua@19064
    68
fun element name atts cs =
obua@19064
    69
  let val elem = space_implode " " (name :: map attribute atts) in
obua@19064
    70
    if null cs then enclose "<" "/>" elem
obua@19064
    71
    else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name
obua@19064
    72
  end;
obua@19064
    73
obua@19064
    74
(** explicit XML trees **)
obua@19064
    75
obua@19064
    76
datatype tree =
obua@19064
    77
    Elem of string * (string * string) list * tree list
obua@19064
    78
  | Text of string;
obua@19064
    79
obua@19064
    80
fun string_of_tree tree =
obua@19064
    81
  let
obua@19064
    82
    fun string_of (Elem (name, atts, ts)) buf =
obua@19064
    83
        let val buf' =
obua@19064
    84
          buf |> Buffer.add "<"
obua@19064
    85
          |> fold Buffer.add (separate " " (name :: map attribute atts))
obua@19064
    86
        in
obua@19064
    87
          if null ts then
obua@19064
    88
            buf' |> Buffer.add "/>"
obua@19064
    89
          else
obua@19064
    90
            buf' |> Buffer.add ">"
obua@19064
    91
            |> fold string_of ts
obua@19064
    92
            |> Buffer.add "</" |> Buffer.add name |> Buffer.add ">"
obua@19064
    93
        end
obua@19064
    94
      | string_of (Text s) buf = Buffer.add (text s) buf;
obua@19064
    95
  in Buffer.content (string_of tree Buffer.empty) end;
obua@19064
    96
obua@19064
    97
(** XML parsing **)
obua@19064
    98
obua@19089
    99
fun beginning n xs = Symbol.beginning n (Seq.take_at_most xs n)
obua@19064
   100
obua@19064
   101
fun err s xs =
obua@19064
   102
  "XML parsing error: " ^ s ^ "\nfound: " ^ quote (beginning 100 xs) ;
obua@19064
   103
obua@19064
   104
val scan_whspc = Scan.any Symbol.is_blank;
obua@19064
   105
obua@19064
   106
val scan_special = $$ "&" ^^ scan_id ^^ $$ ";" >> decode;
obua@19064
   107
obua@19064
   108
val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
wenzelm@23784
   109
  (scan_special || Scan.one Symbol.is_regular)) >> implode;
obua@19064
   110
obua@19064
   111
val parse_cdata = Scan.this_string "<![CDATA[" |--
wenzelm@23784
   112
  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.is_regular)) >>
obua@19064
   113
    implode) --| Scan.this_string "]]>";
obua@19064
   114
obua@19064
   115
val parse_att =
obua@19064
   116
    scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
obua@19064
   117
    (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
wenzelm@23784
   118
    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s) >> snd);
obua@19064
   119
obua@19064
   120
val parse_comment = Scan.this_string "<!--" --
wenzelm@23784
   121
  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --
obua@19064
   122
  Scan.this_string "-->";
obua@19064
   123
obua@19064
   124
val scan_comment_whspc = 
obua@19064
   125
    (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
obua@19064
   126
obua@19064
   127
val parse_pi = Scan.this_string "<?" |--
wenzelm@23784
   128
  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.is_regular)) --|
obua@19064
   129
  Scan.this_string "?>";
obua@19064
   130
obua@19064
   131
fun parse_content xs =
obua@19064
   132
  ((Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) [] --
obua@19064
   133
    (Scan.repeat ((* scan_whspc |-- *)
obua@19064
   134
       (   parse_elem >> single
obua@19064
   135
        || parse_cdata >> (single o Text)
obua@19064
   136
        || parse_pi >> K []
obua@19064
   137
        || parse_comment >> K []) --
obua@19064
   138
       Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) []
wenzelm@32952
   139
         >> op @) >> flat) >> op @)(* --| scan_whspc*)) xs
obua@19064
   140
obua@19064
   141
and parse_elem xs =
obua@19064
   142
  ($$ "<" |-- scan_id --
obua@19064
   143
    Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
obua@19064
   144
      !! (err "Expected > or />")
obua@19064
   145
        (Scan.this_string "/>" >> K []
obua@19064
   146
         || $$ ">" |-- parse_content --|
obua@19064
   147
            !! (err ("Expected </" ^ s ^ ">"))
obua@19064
   148
              (Scan.this_string ("</" ^ s) --| scan_whspc --| $$ ">"))) >>
obua@19064
   149
    (fn ((s, atts), ts) => Elem (s, atts, ts))) xs;
obua@19064
   150
obua@19064
   151
val parse_document =
obua@19064
   152
  Scan.option (Scan.this_string "<!DOCTYPE" -- scan_whspc |--
obua@19064
   153
    (Scan.repeat (Scan.unless ($$ ">")
wenzelm@23784
   154
      (Scan.one Symbol.is_regular)) >> implode) --| $$ ">" --| scan_whspc) --
obua@19064
   155
  parse_elem;
obua@19064
   156
obua@19064
   157
fun tree_of_string s =
obua@19064
   158
    let
wenzelm@32960
   159
        val seq = Seq.fromString s
wenzelm@32960
   160
        val scanner = !! (err "Malformed element") (scan_whspc |-- parse_elem --| scan_whspc)
wenzelm@32960
   161
        val (x, toks) = scanner seq
obua@19064
   162
    in
wenzelm@32960
   163
        if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
obua@19064
   164
    end
obua@19089
   165
obua@19089
   166
(* More efficient saving and loading of xml trees employing a proprietary external format *)
obua@19089
   167
obua@19089
   168
fun write_lstring s buf = buf |> Buffer.add (string_of_int (size s)) |> Buffer.add " " |> Buffer.add s
obua@19089
   169
fun parse_lstring toks = (scan_nat --| one Symbol.is_blank :-- (fn i => repeat_fixed i (one (K true))) >> snd >> implode) toks
obua@19089
   170
obua@19089
   171
fun write_list w l buf = buf |> Buffer.add (string_of_int (length l)) |> Buffer.add " " |> fold w l     
obua@19089
   172
fun parse_list sc = scan_nat --| one Symbol.is_blank :-- (fn i => repeat_fixed i sc) >> snd
obua@19089
   173
obua@19089
   174
fun write_tree (Text s) buf = buf |> Buffer.add "T" |> write_lstring s
obua@19089
   175
  | write_tree (Elem (name, attrs, children)) buf = 
obua@19089
   176
    buf |> Buffer.add "E" 
wenzelm@32960
   177
        |> write_lstring name 
wenzelm@32960
   178
        |> write_list (fn (a,b) => fn buf => buf |> write_lstring a |> write_lstring b) attrs 
wenzelm@32960
   179
        |> write_list write_tree children
obua@19089
   180
obua@19089
   181
fun parse_tree toks = (one (K true) :-- (fn "T" => parse_lstring >> Text | "E" => parse_elem | _ => raise SyntaxError) >> snd) toks
obua@19089
   182
and parse_elem toks = (parse_lstring -- parse_list (parse_lstring -- parse_lstring) -- parse_list parse_tree >> (fn ((n, a), c) => Elem (n,a,c))) toks
obua@19089
   183
obua@19089
   184
fun encoded_string_of_tree tree = Buffer.content (write_tree tree Buffer.empty)
obua@19089
   185
obua@19089
   186
fun tree_of_encoded_string s = 
obua@19089
   187
    let
wenzelm@32960
   188
        fun print (a,b) = writeln (a^" "^(string_of_int b))
wenzelm@32960
   189
        val _ = print ("length of encoded string: ", size s)
wenzelm@32960
   190
        val _ = writeln "Seq.fromString..."
wenzelm@32960
   191
        val seq = timeit (fn () => Seq.fromString s)
wenzelm@32960
   192
        val  _ = print ("length of sequence", timeit (fn () => Seq.length seq))
wenzelm@32960
   193
        val scanner = !! (err "Malformed encoded xml") parse_tree
wenzelm@32960
   194
        val (x, toks) = scanner seq
obua@19089
   195
    in
wenzelm@32960
   196
        if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
wenzelm@32960
   197
    end        
obua@19089
   198
obua@19064
   199
end;