equal
deleted
inserted
replaced
725 } |
725 } |
726 |
726 |
727 |
727 |
728 sealed case class Markup(name: String, properties: Properties.T) |
728 sealed case class Markup(name: String, properties: Properties.T) |
729 { |
729 { |
|
730 def is_empty: Boolean = name.isEmpty |
|
731 |
730 def markup(s: String): String = |
732 def markup(s: String): String = |
731 YXML.string_of_tree(XML.Elem(this, List(XML.Text(s)))) |
733 YXML.string_of_tree(XML.Elem(this, List(XML.Text(s)))) |
732 |
734 |
733 def update_properties(more_props: Properties.T): Markup = |
735 def update_properties(more_props: Properties.T): Markup = |
734 if (more_props.isEmpty) this |
736 if (more_props.isEmpty) this |