69227
|
1 |
{- generated by Isabelle -}
|
69226
|
2 |
|
69225
|
3 |
{- Title: Tools/Haskell/XML.hs
|
|
4 |
Author: Makarius
|
|
5 |
LICENSE: BSD 3-clause (Isabelle)
|
|
6 |
|
|
7 |
Untyped XML trees and representation of ML values.
|
|
8 |
-}
|
|
9 |
|
|
10 |
module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
|
|
11 |
where
|
|
12 |
|
|
13 |
import qualified Data.List as List
|
|
14 |
|
|
15 |
import Isabelle.Library
|
|
16 |
import qualified Isabelle.Properties as Properties
|
|
17 |
import qualified Isabelle.Markup as Markup
|
|
18 |
import qualified Isabelle.Buffer as Buffer
|
|
19 |
|
|
20 |
|
|
21 |
{- types -}
|
|
22 |
|
|
23 |
type Attributes = Properties.T
|
|
24 |
type Body = [Tree]
|
|
25 |
data Tree = Elem Markup.T Body | Text String
|
|
26 |
|
|
27 |
|
|
28 |
{- wrapped elements -}
|
|
29 |
|
69236
|
30 |
wrap_elem (((a, atts), body1), body2) =
|
|
31 |
Elem ("xml_elem", ("xml_name", a) : atts) (Elem ("xml_body", []) body1 : body2)
|
69225
|
32 |
|
69236
|
33 |
unwrap_elem
|
|
34 |
(Elem ("xml_elem", ("xml_name", a) : atts) (Elem ("xml_body", []) body1 : body2)) =
|
|
35 |
Just (((a, atts), body1), body2)
|
69225
|
36 |
unwrap_elem _ = Nothing
|
|
37 |
|
|
38 |
|
|
39 |
{- text content -}
|
|
40 |
|
|
41 |
add_content tree =
|
|
42 |
case unwrap_elem tree of
|
|
43 |
Just (_, ts) -> fold add_content ts
|
|
44 |
Nothing ->
|
|
45 |
case tree of
|
|
46 |
Elem _ ts -> fold add_content ts
|
|
47 |
Text s -> Buffer.add s
|
|
48 |
|
|
49 |
content_of body = Buffer.empty |> fold add_content body |> Buffer.content
|
|
50 |
|
|
51 |
|
|
52 |
{- string representation -}
|
|
53 |
|
|
54 |
encode '<' = "<"
|
|
55 |
encode '>' = ">"
|
|
56 |
encode '&' = "&"
|
|
57 |
encode '\'' = "'"
|
|
58 |
encode '\"' = """
|
|
59 |
encode c = [c]
|
|
60 |
|
|
61 |
instance Show Tree where
|
|
62 |
show tree =
|
|
63 |
Buffer.empty |> show_tree tree |> Buffer.content
|
|
64 |
where
|
|
65 |
show_tree (Elem (name, atts) []) =
|
|
66 |
Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
|
|
67 |
show_tree (Elem (name, atts) ts) =
|
|
68 |
Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
|
|
69 |
fold show_tree ts #>
|
|
70 |
Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
|
|
71 |
show_tree (Text s) = Buffer.add (show_text s)
|
|
72 |
|
|
73 |
show_elem name atts =
|
|
74 |
unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
|
|
75 |
|
|
76 |
show_text = concatMap encode
|