src/Pure/PIDE/yxml.ML
author wenzelm
Tue, 10 Jan 2012 23:26:27 +0100
changeset 46178 1c5c88f6feb5
parent 44698 0385292321a0
child 46831 4a6085849a37
permissions -rw-r--r--
clarified Isabelle_Rendering vs. physical painting; discontinued slightly odd object-oriented Markup_Tree.Cumulate/Select;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
44698
0385292321a0 moved XML/YXML to src/Pure/PIDE;
wenzelm
parents: 43782
diff changeset
     1
(*  Title:      Pure/PIDE/yxml.ML
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
     3
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
     4
Efficient text representation of XML trees using extra characters X
44698
0385292321a0 moved XML/YXML to src/Pure/PIDE;
wenzelm
parents: 43782
diff changeset
     5
and Y -- no escaping, may nest marked text verbatim.  Suitable for
0385292321a0 moved XML/YXML to src/Pure/PIDE;
wenzelm
parents: 43782
diff changeset
     6
direct inlining into plain text.
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
     7
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
     8
Markup <elem att="val" ...>...body...</elem> is encoded as:
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
     9
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    10
  X Y name Y att=val ... X
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    11
  ...
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    12
  body
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    13
  ...
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    14
  X Y X
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    15
*)
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    16
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    17
signature YXML =
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    18
sig
43777
22c87ff1b8a9 tuned signature -- less cryptic ASCII names;
wenzelm
parents: 43772
diff changeset
    19
  val X: Symbol.symbol
22c87ff1b8a9 tuned signature -- less cryptic ASCII names;
wenzelm
parents: 43772
diff changeset
    20
  val Y: Symbol.symbol
43772
c825594fd0c1 clarified YXML.embed_controls -- this is idempotent and cannot be nested;
wenzelm
parents: 43731
diff changeset
    21
  val embed_controls: string -> string
43731
70072780e095 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents: 43728
diff changeset
    22
  val detect: string -> bool
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    23
  val output_markup: Markup.T -> string * string
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    24
  val element: string -> XML.attributes -> string list -> string
43728
152ce7114396 YXML.string_of_body convenience;
wenzelm
parents: 43615
diff changeset
    25
  val string_of_body: XML.body -> string
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    26
  val string_of: XML.tree -> string
38266
492d377ecfe2 type XML.body as basic data representation language;
wenzelm
parents: 38265
diff changeset
    27
  val parse_body: string -> XML.body
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    28
  val parse: string -> XML.tree
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    29
end;
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    30
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    31
structure YXML: YXML =
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    32
struct
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    33
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    34
(** string representation **)
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    35
38265
cc9fde54311f renamed YXML.binary_text to YXML.escape_controls to emphasize what it actually does;
wenzelm
parents: 38228
diff changeset
    36
(* idempotent recoding of certain low ASCII control characters *)
34095
c2f176a38448 robust representation of low ASCII control characters within XML/YXML text;
wenzelm
parents: 31469
diff changeset
    37
c2f176a38448 robust representation of low ASCII control characters within XML/YXML text;
wenzelm
parents: 31469
diff changeset
    38
fun pseudo_utf8 c =
c2f176a38448 robust representation of low ASCII control characters within XML/YXML text;
wenzelm
parents: 31469
diff changeset
    39
  if Symbol.is_ascii_control c
c2f176a38448 robust representation of low ASCII control characters within XML/YXML text;
wenzelm
parents: 31469
diff changeset
    40
  then chr 192 ^ chr (128 + ord c)
c2f176a38448 robust representation of low ASCII control characters within XML/YXML text;
wenzelm
parents: 31469
diff changeset
    41
  else c;
c2f176a38448 robust representation of low ASCII control characters within XML/YXML text;
wenzelm
parents: 31469
diff changeset
    42
43772
c825594fd0c1 clarified YXML.embed_controls -- this is idempotent and cannot be nested;
wenzelm
parents: 43731
diff changeset
    43
fun embed_controls str =
34095
c2f176a38448 robust representation of low ASCII control characters within XML/YXML text;
wenzelm
parents: 31469
diff changeset
    44
  if exists_string Symbol.is_ascii_control str
c2f176a38448 robust representation of low ASCII control characters within XML/YXML text;
wenzelm
parents: 31469
diff changeset
    45
  then translate_string pseudo_utf8 str
c2f176a38448 robust representation of low ASCII control characters within XML/YXML text;
wenzelm
parents: 31469
diff changeset
    46
  else str;
c2f176a38448 robust representation of low ASCII control characters within XML/YXML text;
wenzelm
parents: 31469
diff changeset
    47
c2f176a38448 robust representation of low ASCII control characters within XML/YXML text;
wenzelm
parents: 31469
diff changeset
    48
26547
1112375f6a69 tuned comments;
wenzelm
parents: 26540
diff changeset
    49
(* markers *)
1112375f6a69 tuned comments;
wenzelm
parents: 26540
diff changeset
    50
43777
22c87ff1b8a9 tuned signature -- less cryptic ASCII names;
wenzelm
parents: 43772
diff changeset
    51
val X = chr 5;
22c87ff1b8a9 tuned signature -- less cryptic ASCII names;
wenzelm
parents: 43772
diff changeset
    52
val Y = chr 6;
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    53
val XY = X ^ Y;
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    54
val XYX = XY ^ X;
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    55
43782
834de29572d5 clarified YXML.detect;
wenzelm
parents: 43777
diff changeset
    56
val detect = exists_string (fn s => s = X orelse s = Y);
43731
70072780e095 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
wenzelm
parents: 43728
diff changeset
    57
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    58
26547
1112375f6a69 tuned comments;
wenzelm
parents: 26540
diff changeset
    59
(* output *)
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    60
27884
10c927e4abf5 output_markup: check Markup.is_none;
wenzelm
parents: 27798
diff changeset
    61
fun output_markup (markup as (name, atts)) =
38474
e498dc2eb576 uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents: 38266
diff changeset
    62
  if Markup.is_empty markup then Markup.no_output
27884
10c927e4abf5 output_markup: check Markup.is_none;
wenzelm
parents: 27798
diff changeset
    63
  else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    64
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    65
fun element name atts body =
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    66
  let val (pre, post) = output_markup (name, atts)
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    67
  in pre ^ implode body ^ post end;
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    68
43728
152ce7114396 YXML.string_of_body convenience;
wenzelm
parents: 43615
diff changeset
    69
fun string_of_body body =
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    70
  let
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    71
    fun attrib (a, x) =
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    72
      Buffer.add Y #>
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    73
      Buffer.add a #> Buffer.add "=" #> Buffer.add x;
38228
ada3ab6b9085 simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents: 34095
diff changeset
    74
    fun tree (XML.Elem ((name, atts), ts)) =
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    75
          Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
43728
152ce7114396 YXML.string_of_body convenience;
wenzelm
parents: 43615
diff changeset
    76
          trees ts #>
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    77
          Buffer.add XYX
43728
152ce7114396 YXML.string_of_body convenience;
wenzelm
parents: 43615
diff changeset
    78
      | tree (XML.Text s) = Buffer.add s
152ce7114396 YXML.string_of_body convenience;
wenzelm
parents: 43615
diff changeset
    79
    and trees ts = fold tree ts;
152ce7114396 YXML.string_of_body convenience;
wenzelm
parents: 43615
diff changeset
    80
  in Buffer.empty |> trees body |> Buffer.content end;
152ce7114396 YXML.string_of_body convenience;
wenzelm
parents: 43615
diff changeset
    81
152ce7114396 YXML.string_of_body convenience;
wenzelm
parents: 43615
diff changeset
    82
val string_of = string_of_body o single;
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    83
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    84
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    85
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    86
(** efficient YXML parsing **)
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    87
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    88
local
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
    89
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    90
(* splitting *)
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    91
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    92
fun is_char s c = ord s = Char.ord c;
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    93
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    94
val split_string =
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    95
  Substring.full #>
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    96
  Substring.tokens (is_char X) #>
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    97
  map (Substring.fields (is_char Y) #> map Substring.string);
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    98
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
    99
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
   100
(* structural errors *)
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   101
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   102
fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   103
fun err_attribute () = err "bad attribute";
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   104
fun err_element () = err "bad element";
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   105
fun err_unbalanced "" = err "unbalanced element"
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   106
  | err_unbalanced name = err ("unbalanced element " ^ quote name);
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   107
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   108
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   109
(* stack operations *)
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   110
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   111
fun add x ((elem, body) :: pending) = (elem, x :: body) :: pending;
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   112
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   113
fun push "" _ _ = err_element ()
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   114
  | push name atts pending = ((name, atts), []) :: pending;
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   115
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   116
fun pop ((("", _), _) :: _) = err_unbalanced ""
38228
ada3ab6b9085 simplified type XML.tree: embed Markup.T directly, avoid slightly odd triple;
wenzelm
parents: 34095
diff changeset
   117
  | pop ((markup, body) :: pending) = add (XML.Elem (markup, rev body)) pending;
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   118
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   119
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
   120
(* parsing *)
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   121
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   122
fun parse_attrib s =
28025
d9fcab768496 replaced find_substring by first_field;
wenzelm
parents: 28023
diff changeset
   123
  (case first_field "=" s of
28023
92dd3ad302b7 simplified parse_attrib (find_substring instead of space_explode);
wenzelm
parents: 27932
diff changeset
   124
    NONE => err_attribute ()
28025
d9fcab768496 replaced find_substring by first_field;
wenzelm
parents: 28023
diff changeset
   125
  | SOME ("", _) => err_attribute ()
d9fcab768496 replaced find_substring by first_field;
wenzelm
parents: 28023
diff changeset
   126
  | SOME att => att);
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   127
26540
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
   128
fun parse_chunk ["", ""] = pop
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
   129
  | parse_chunk ("" :: name :: atts) = push name (map parse_attrib atts)
173d548ce9d2 replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
wenzelm
parents: 26528
diff changeset
   130
  | parse_chunk txts = fold (add o XML.Text) txts;
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   131
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   132
in
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   133
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   134
fun parse_body source =
43615
8e0f6cfa8eb2 reverted ce00462f,b3759dce, 7a165592: unwanted generalisation
noschinl
parents: 42355
diff changeset
   135
  (case fold parse_chunk (split_string source) [(("", []), [])] of
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   136
    [(("", _), result)] => rev result
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   137
  | ((name, _), _) :: _ => err_unbalanced name);
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   138
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   139
fun parse source =
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   140
  (case parse_body source of
27798
b96c73f11a23 YXML.parse: allow text without markup, potentially empty;
wenzelm
parents: 26684
diff changeset
   141
    [result] => result
b96c73f11a23 YXML.parse: allow text without markup, potentially empty;
wenzelm
parents: 26684
diff changeset
   142
  | [] => XML.Text ""
b96c73f11a23 YXML.parse: allow text without markup, potentially empty;
wenzelm
parents: 26684
diff changeset
   143
  | _ => err "multiple results");
26528
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   144
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   145
end;
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   146
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   147
end;
944f9bf26d2d Why XML notation?
wenzelm
parents:
diff changeset
   148