1 {- generated by Isabelle -} |
|
2 |
|
3 {- Title: Tools/Haskell/YXML.hs |
|
4 Author: Makarius |
|
5 LICENSE: BSD 3-clause (Isabelle) |
|
6 |
|
7 Efficient text representation of XML trees. Suitable for direct |
|
8 inlining into plain text. |
|
9 |
|
10 See also "$ISABELLE_HOME/src/Pure/PIDE/yxml.ML". |
|
11 -} |
|
12 |
|
13 module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup, |
|
14 buffer_body, buffer, string_of_body, string_of, parse_body, parse) |
|
15 where |
|
16 |
|
17 import qualified Data.Char as Char |
|
18 import qualified Data.List as List |
|
19 |
|
20 import Isabelle.Library |
|
21 import qualified Isabelle.Markup as Markup |
|
22 import qualified Isabelle.XML as XML |
|
23 import qualified Isabelle.Buffer as Buffer |
|
24 |
|
25 |
|
26 {- markers -} |
|
27 |
|
28 charX, charY :: Char |
|
29 charX = Char.chr 5 |
|
30 charY = Char.chr 6 |
|
31 |
|
32 strX, strY, strXY, strXYX :: String |
|
33 strX = [charX] |
|
34 strY = [charY] |
|
35 strXY = strX ++ strY |
|
36 strXYX = strXY ++ strX |
|
37 |
|
38 detect :: String -> Bool |
|
39 detect = any (\c -> c == charX || c == charY) |
|
40 |
|
41 |
|
42 {- output -} |
|
43 |
|
44 output_markup :: Markup.T -> Markup.Output |
|
45 output_markup markup@(name, atts) = |
|
46 if Markup.is_empty markup then Markup.no_output |
|
47 else (strXY ++ name ++ concatMap (\(a, x) -> strY ++ a ++ "=" ++ x) atts ++ strX, strXYX) |
|
48 |
|
49 buffer_attrib (a, x) = |
|
50 Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x |
|
51 |
|
52 buffer_body :: XML.Body -> Buffer.T -> Buffer.T |
|
53 buffer_body = fold buffer |
|
54 |
|
55 buffer :: XML.Tree -> Buffer.T -> Buffer.T |
|
56 buffer (XML.Elem ((name, atts), ts)) = |
|
57 Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #> |
|
58 buffer_body ts #> |
|
59 Buffer.add strXYX |
|
60 buffer (XML.Text s) = Buffer.add s |
|
61 |
|
62 string_of_body :: XML.Body -> String |
|
63 string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content |
|
64 |
|
65 string_of :: XML.Tree -> String |
|
66 string_of = string_of_body . single |
|
67 |
|
68 |
|
69 {- parse -} |
|
70 |
|
71 -- split: fields or non-empty tokens |
|
72 |
|
73 split :: Bool -> Char -> String -> [String] |
|
74 split _ _ [] = [] |
|
75 split fields sep str = splitting str |
|
76 where |
|
77 splitting rest = |
|
78 case span (/= sep) rest of |
|
79 (_, []) -> cons rest [] |
|
80 (prfx, _ : rest') -> cons prfx (splitting rest') |
|
81 cons item = if fields || not (null item) then (:) item else id |
|
82 |
|
83 |
|
84 -- structural errors |
|
85 |
|
86 err msg = error ("Malformed YXML: " ++ msg) |
|
87 err_attribute = err "bad attribute" |
|
88 err_element = err "bad element" |
|
89 err_unbalanced "" = err "unbalanced element" |
|
90 err_unbalanced name = err ("unbalanced element " ++ quote name) |
|
91 |
|
92 |
|
93 -- stack operations |
|
94 |
|
95 add x ((elem, body) : pending) = (elem, x : body) : pending |
|
96 |
|
97 push "" _ _ = err_element |
|
98 push name atts pending = ((name, atts), []) : pending |
|
99 |
|
100 pop ((("", _), _) : _) = err_unbalanced "" |
|
101 pop ((markup, body) : pending) = add (XML.Elem (markup, reverse body)) pending |
|
102 |
|
103 |
|
104 -- parsing |
|
105 |
|
106 parse_attrib s = |
|
107 case List.elemIndex '=' s of |
|
108 Just i | i > 0 -> (take i s, drop (i + 1) s) |
|
109 _ -> err_attribute |
|
110 |
|
111 parse_chunk ["", ""] = pop |
|
112 parse_chunk ("" : name : atts) = push name (map parse_attrib atts) |
|
113 parse_chunk txts = fold (add . XML.Text) txts |
|
114 |
|
115 parse_body :: String -> XML.Body |
|
116 parse_body source = |
|
117 case fold parse_chunk chunks [(("", []), [])] of |
|
118 [(("", _), result)] -> reverse result |
|
119 ((name, _), _) : _ -> err_unbalanced name |
|
120 where chunks = split False charX source |> map (split True charY) |
|
121 |
|
122 parse :: String -> XML.Tree |
|
123 parse source = |
|
124 case parse_body source of |
|
125 [result] -> result |
|
126 [] -> XML.Text "" |
|
127 _ -> err "multiple results" |
|