wenzelm@26528: (*  Title:      Pure/General/yxml.ML
wenzelm@26528:     ID:         $Id$
wenzelm@26528:     Author:     Makarius
wenzelm@26528: 
wenzelm@26540: Efficient text representation of XML trees using extra characters X
wenzelm@26540: and Y -- no escaping, may nest marked text verbatim.
wenzelm@26528: 
wenzelm@26540: Markup <elem att="val" ...>...body...</elem> is encoded as:
wenzelm@26540: 
wenzelm@26540:   X Y name Y att=val ... X
wenzelm@26528:   ...
wenzelm@26528:   body
wenzelm@26528:   ...
wenzelm@26540:   X Y X
wenzelm@26528: *)
wenzelm@26528: 
wenzelm@26528: signature YXML =
wenzelm@26528: sig
wenzelm@26528:   val detect: string -> bool
wenzelm@26540:   val output_markup: Markup.T -> string * string
wenzelm@26528:   val element: string -> XML.attributes -> string list -> string
wenzelm@26528:   val string_of: XML.tree -> string
wenzelm@26528:   val parse_body: string -> XML.tree list
wenzelm@26528:   val parse: string -> XML.tree
wenzelm@26528: end;
wenzelm@26528: 
wenzelm@26528: structure YXML: YXML =
wenzelm@26528: struct
wenzelm@26528: 
wenzelm@26540: (** string representation **)
wenzelm@26528: 
wenzelm@26547: (* markers *)
wenzelm@26547: 
wenzelm@26540: val X = Symbol.ENQ;
wenzelm@26540: val Y = Symbol.ACK;
wenzelm@26540: val XY = X ^ Y;
wenzelm@26540: val XYX = XY ^ X;
wenzelm@26528: 
wenzelm@26540: val detect = String.isPrefix XY;
wenzelm@26528: 
wenzelm@26528: 
wenzelm@26547: (* output *)
wenzelm@26540: 
wenzelm@27884: fun output_markup (markup as (name, atts)) =
wenzelm@27884:   if Markup.is_none markup then ("", "")
wenzelm@27884:   else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
wenzelm@26540: 
wenzelm@26528: fun element name atts body =
wenzelm@26540:   let val (pre, post) = output_markup (name, atts)
wenzelm@26540:   in pre ^ implode body ^ post end;
wenzelm@26528: 
wenzelm@26528: fun string_of t =
wenzelm@26528:   let
wenzelm@26528:     fun attrib (a, x) =
wenzelm@26540:       Buffer.add Y #>
wenzelm@26528:       Buffer.add a #> Buffer.add "=" #> Buffer.add x;
wenzelm@26528:     fun tree (XML.Elem (name, atts, ts)) =
wenzelm@26540:           Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
wenzelm@26528:           fold tree ts #>
wenzelm@26540:           Buffer.add XYX
wenzelm@28033:       | tree (XML.Text s) = Buffer.add s;
wenzelm@26528:   in Buffer.empty |> tree t |> Buffer.content end;
wenzelm@26528: 
wenzelm@26528: 
wenzelm@26540: 
wenzelm@26540: (** efficient YXML parsing **)
wenzelm@26528: 
wenzelm@26528: local
wenzelm@26528: 
wenzelm@26540: (* splitting *)
wenzelm@26540: 
wenzelm@26540: fun is_char s c = ord s = Char.ord c;
wenzelm@26540: 
wenzelm@26540: val split_string =
wenzelm@26540:   Substring.full #>
wenzelm@26540:   Substring.tokens (is_char X) #>
wenzelm@26540:   map (Substring.fields (is_char Y) #> map Substring.string);
wenzelm@26540: 
wenzelm@26540: 
wenzelm@26540: (* structural errors *)
wenzelm@26528: 
wenzelm@26528: fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
wenzelm@26528: fun err_attribute () = err "bad attribute";
wenzelm@26528: fun err_element () = err "bad element";
wenzelm@26528: fun err_unbalanced "" = err "unbalanced element"
wenzelm@26528:   | err_unbalanced name = err ("unbalanced element " ^ quote name);
wenzelm@26528: 
wenzelm@26528: 
wenzelm@26528: (* stack operations *)
wenzelm@26528: 
wenzelm@26528: fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
wenzelm@26528: 
wenzelm@26528: fun push "" _ _ = err_element ()
wenzelm@26528:   | push name atts pending = ((name, atts), []) :: pending;
wenzelm@26528: 
wenzelm@26528: fun pop ((("", _), _) :: _) = err_unbalanced ""
wenzelm@26528:   | pop (((name, atts), body) :: pending) = add (XML.Elem (name, atts, rev body)) pending;
wenzelm@26528: 
wenzelm@26528: 
wenzelm@26540: (* parsing *)
wenzelm@26528: 
wenzelm@26528: fun parse_attrib s =
wenzelm@28025:   (case first_field "=" s of
wenzelm@28023:     NONE => err_attribute ()
wenzelm@28025:   | SOME ("", _) => err_attribute ()
wenzelm@28025:   | SOME att => att);
wenzelm@26528: 
wenzelm@26540: fun parse_chunk ["", ""] = pop
wenzelm@26540:   | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
wenzelm@26540:   | parse_chunk txts = fold (add o XML.Text) txts;
wenzelm@26528: 
wenzelm@26528: in
wenzelm@26528: 
wenzelm@26528: fun parse_body source =
wenzelm@26540:   (case fold parse_chunk (split_string source) [(("", []), [])] of
wenzelm@26528:     [(("", _), result)] => rev result
wenzelm@26528:   | ((name, _), _) :: _ => err_unbalanced name);
wenzelm@26528: 
wenzelm@26528: fun parse source =
wenzelm@26528:   (case parse_body source of
wenzelm@27798:     [result] => result
wenzelm@27798:   | [] => XML.Text ""
wenzelm@27798:   | _ => err "multiple results");
wenzelm@26528: 
wenzelm@26528: end;
wenzelm@26528: 
wenzelm@26528: end;
wenzelm@26528: