equal
deleted
inserted
replaced
27 case class Elem(markup: Markup, body: List[Tree]) extends Tree |
27 case class Elem(markup: Markup, body: List[Tree]) extends Tree |
28 case class Text(content: String) extends Tree |
28 case class Text(content: String) extends Tree |
29 |
29 |
30 def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body) |
30 def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body) |
31 def elem(name: String) = Elem(Markup(name, Nil), Nil) |
31 def elem(name: String) = Elem(Markup(name, Nil), Nil) |
|
32 |
|
33 type Body = List[Tree] |
32 |
34 |
33 |
35 |
34 /* string representation */ |
36 /* string representation */ |
35 |
37 |
36 private def append_text(text: String, s: StringBuilder) { |
38 private def append_text(text: String, s: StringBuilder) { |