equal
deleted
inserted
replaced
81 def output(tree: XML.Tree): String = output(List(tree)) |
81 def output(tree: XML.Tree): String = output(List(tree)) |
82 |
82 |
83 |
83 |
84 /* attributes */ |
84 /* attributes */ |
85 |
85 |
86 def id(s: String): Properties.Entry = ("id" -> s) |
86 def id(s: String): XML.Attribute = ("id" -> s) |
|
87 def width(w: Int): XML.Attribute = ("width" -> w.toString) |
|
88 def height(h: Int): XML.Attribute = ("height" -> h.toString) |
87 |
89 |
88 |
90 |
89 /* structured markup operators */ |
91 /* structured markup operators */ |
90 |
92 |
91 def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt)) |
93 def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt)) |