src/Tools/Haskell/XML.hs
author wenzelm
Mon Nov 05 11:29:11 2018 +0100 (7 months ago)
changeset 69236 a75aab6d785b
parent 69234 2dec32c7313f
child 69280 e1d01b351724
permissions -rw-r--r--
tuned;
     1 {- generated by Isabelle -}
     2 
     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 
    30 wrap_elem (((a, atts), body1), body2) =
    31   Elem ("xml_elem", ("xml_name", a) : atts) (Elem ("xml_body", []) body1 : body2)
    32 
    33 unwrap_elem
    34   (Elem ("xml_elem", ("xml_name", a) : atts) (Elem ("xml_body", []) body1 : body2)) =
    35   Just (((a, atts), body1), body2)
    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 '<' = "&lt;"
    55 encode '>' = "&gt;"
    56 encode '&' = "&amp;"
    57 encode '\'' = "&apos;"
    58 encode '\"' = "&quot;"
    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