src/Tools/Haskell/XML.hs
author wenzelm
Mon, 12 Nov 2018 15:14:12 +0100
changeset 69289 bf6937af7fe8
parent 69280 e1d01b351724
child 69290 fb77612d11eb
permissions -rw-r--r--
clarified signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69227
71b48b749836 tuned message (e.g. see Options.save_prefs);
wenzelm
parents: 69226
diff changeset
     1
{- generated by Isabelle -}
69226
68f5dc2275ac tuned whitespace;
wenzelm
parents: 69225
diff changeset
     2
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     3
{-  Title:      Tools/Haskell/XML.hs
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     4
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     5
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     6
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
     7
Untyped XML trees and representation of ML values.
69280
e1d01b351724 more formal references;
wenzelm
parents: 69236
diff changeset
     8
e1d01b351724 more formal references;
wenzelm
parents: 69236
diff changeset
     9
See also "$ISABELLE_HOME/src/Pure/PIDE/xml.ML".
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    10
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    11
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    12
module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    13
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    14
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    15
import qualified Data.List as List
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    16
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    17
import Isabelle.Library
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    18
import qualified Isabelle.Properties as Properties
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    19
import qualified Isabelle.Markup as Markup
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    20
import qualified Isabelle.Buffer as Buffer
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    21
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    22
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    23
{- types -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    24
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    25
type Attributes = Properties.T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    26
type Body = [Tree]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    27
data Tree = Elem Markup.T Body | Text String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    28
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    29
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    30
{- wrapped elements -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    31
69236
wenzelm
parents: 69234
diff changeset
    32
wrap_elem (((a, atts), body1), body2) =
wenzelm
parents: 69234
diff changeset
    33
  Elem ("xml_elem", ("xml_name", a) : atts) (Elem ("xml_body", []) body1 : body2)
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    34
69236
wenzelm
parents: 69234
diff changeset
    35
unwrap_elem
wenzelm
parents: 69234
diff changeset
    36
  (Elem ("xml_elem", ("xml_name", a) : atts) (Elem ("xml_body", []) body1 : body2)) =
wenzelm
parents: 69234
diff changeset
    37
  Just (((a, atts), body1), body2)
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    38
unwrap_elem _ = Nothing
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    39
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    40
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    41
{- text content -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    42
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    43
add_content tree =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    44
  case unwrap_elem tree of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    45
    Just (_, ts) -> fold add_content ts
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    46
    Nothing ->
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    47
      case tree of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    48
        Elem _ ts -> fold add_content ts
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    49
        Text s -> Buffer.add s
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    50
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    51
content_of body = Buffer.empty |> fold add_content body |> Buffer.content
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    52
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    53
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    54
{- string representation -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    55
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    56
encode '<' = "&lt;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    57
encode '>' = "&gt;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    58
encode '&' = "&amp;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    59
encode '\'' = "&apos;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    60
encode '\"' = "&quot;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    61
encode c = [c]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    62
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    63
instance Show Tree where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    64
  show tree =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    65
    Buffer.empty |> show_tree tree |> Buffer.content
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    66
    where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    67
      show_tree (Elem (name, atts) []) =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    68
        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    69
      show_tree (Elem (name, atts) ts) =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    70
        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    71
        fold show_tree ts #>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    72
        Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    73
      show_tree (Text s) = Buffer.add (show_text s)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    74
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    75
      show_elem name atts =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    76
        unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    77
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents:
diff changeset
    78
      show_text = concatMap encode