Impressum yxml.ML Sprache: SML

(*  Title:      Pure/PIDE/yxml.ML
    Author:     Makarius

Efficient text representation of XML trees using extra characters X
and Y -- no escaping, may nest marked text verbatim.  Suitable for
direct inlining into plain text.

Markup <elem att="val" ...>...body...</elem> is encoded as:

  X Y name Y att=val ... X
  ...
  body
  ...
  X Y X
*)

signature YXML =
sig
  include YXML
  val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
  val tree_size: XML.tree -> int
  val body_size: XML.body -> int
  val string_of_body: XML.body -> string
  val string_of: XML.tree -> string
  val bytes_of_body: XML.body -> Bytes.T
  val bytes_of: XML.tree -> Bytes.T
  val write_body: Path.T -> XML.body -> unit
  val output_markup_only: Markup.T -> string
  val output_markup_elem: Markup.T -> (string * string) * string
  val parse_body: string -> XML.body
  val parse_body_bytes: Bytes.T -> XML.body
  val parse: string -> XML.tree
  val parse_bytes: Bytes.T -> XML.tree
  val is_wellformed: string -> bool
end;

structure YXML: YXML =
struct

open YXML;

(** string representation **)

(* traverse *)

fun traverse string =
  let
    fun attrib (a, x) = string Y #> string a #> string "=" #> string x;
    fun tree (XML.Elem (markup as (name, atts), ts)) =
          if Markup.is_empty markup then fold tree ts
          else
            string XY #> string name #> fold attrib atts #> string X #>
            fold tree ts #>
            string XYX
      | tree (XML.Text s) = string s;
  in tree end;

val tree_size = Integer.build o traverse (Integer.add o size);
val body_size = Integer.build o fold (Integer.add o tree_size);

(* output *)

val string_of_body = Buffer.build_content o fold (traverse Buffer.add);
val string_of = string_of_body o single;

val bytes_of_body = Bytes.build o fold (traverse Bytes.add);
val bytes_of = bytes_of_body o single;

fun write_body path body =
  path |> File_Stream.open_output (fn file =>
    fold (traverse (fn s => fn () => File_Stream.output file s)) body ());

(* markup elements *)

val Z = chr 0;
val Z_text = [XML.Text Z];

val output_markup_only = op ^ o output_markup;

fun output_markup_elem markup =
  let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
  in ((bg1, bg2), en) end;

(** efficient YXML parsing **)

local

(* splitting *)

val split_string =
  Substring.full #>
  Substring.tokens (fn c => c = X_char) #>
  map (Substring.fields (fn c => c = Y_char) #> map Substring.string);

val split_bytes =
  Bytes.space_explode X
  #> map_filter (fn "" => NONE | s => SOME (space_explode Y s));

(* structural errors *)

fun err msg = raise Fail ("Malformed YXML: " ^ msg);
fun err_attribute () = err "bad attribute";
fun err_element () = err "bad element";
fun err_unbalanced "" = err "unbalanced element"
  | err_unbalanced name = err ("unbalanced element " ^ quote name);

(* stack operations *)

fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;

fun push "" _ _ = err_element ()
  | push name atts pending = ((name, atts), []) :: pending;

fun pop ((("", _), _) :: _) = err_unbalanced ""
  | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;

(* parsing *)

fun parse_attrib s =
  (case first_field "=" s of
    NONE => err_attribute ()
  | SOME ("", _) => err_attribute ()
  | SOME att => att);

fun parse_chunk ["", ""] = pop
  | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
  | parse_chunk txts = fold (add o XML.Text) txts;

fun parse_body' chunks =
  (case fold parse_chunk chunks [(("", []), [])] of
    [(("", _), result)] => rev result
  | ((name, _), _) :: _ => err_unbalanced name);

fun parse' chunks =
  (case parse_body' chunks of
    [result] => result
  | [] => XML.Text ""
  | _ => err "multiple results");

in

val parse_body = parse_body' o split_string;
val parse_body_bytes = parse_body' o split_bytes;

val parse = parse' o split_string;
val parse_bytes = parse' o split_bytes;

end;

fun is_wellformed s = string_of_body (parse_body s) = s
  handle Fail _ => false;

end;

quality99%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.25Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.