author | wenzelm |
Mon, 08 May 2017 14:30:37 +0200 | |
changeset 65772 | 368399c5d87f |
parent 65771 | 688a7dd22cbb |
child 65773 | 120ef768c84c |
--- a/src/Pure/PIDE/xml.scala Mon May 08 14:08:27 2017 +0200 +++ b/src/Pure/PIDE/xml.scala Mon May 08 14:30:37 2017 +0200 @@ -31,7 +31,7 @@ if (more_attributes.isEmpty) this else Elem(markup.update_properties(more_attributes), body) - def + (att: Attribute): Tree = Elem(markup + att, body) + def + (att: Attribute): Elem = Elem(markup + att, body) } case class Text(content: String) extends Tree