blob: bf0ac551c850a39ac4e77878ed2b7e44fc0b9798 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Dany Fabian
-/
import Std.Data.TreeMap.Basic
import Init.Data.Ord.String
namespace Lean
namespace Xml
@[expose] def Attributes := Std.TreeMap String String
instance : ToString Attributes := ⟨λ as => as.foldl (λ s n v => s ++ s!" {n}=\"{v}\"") ""⟩
mutual
inductive Element
| Element
(name : String)
(attributes : Attributes)
(content : Array Content)
inductive Content
| Element (element : Element)
| Comment (comment : String)
| Character (content : String)
deriving Inhabited
end
mutual
private partial def eToString : Element → String
| Element.Element n a c => s!"<{n}{a}>{c.map cToString |>.foldl (· ++ ·) ""}</{n}>"
private partial def cToString : Content → String
| Content.Element e => eToString e
| Content.Comment c => s!"<!--{c}-->"
| Content.Character c => c
end
instance : ToString Element := ⟨private_decl% eToString⟩
instance : ToString Content := ⟨private_decl% cToString⟩
|
