changeset 60215 | 5fb4990dfc73 |
parent 57912 | dd9550f84106 |
child 61026 | 397354b29935 |
--- a/src/Pure/PIDE/xml.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/PIDE/xml.scala Sun May 03 00:01:10 2015 +0200 @@ -36,9 +36,9 @@ /* wrapped elements */ - val XML_ELEM = "xml_elem"; - val XML_NAME = "xml_name"; - val XML_BODY = "xml_body"; + val XML_ELEM = "xml_elem" + val XML_NAME = "xml_name" + val XML_BODY = "xml_body" object Wrapped_Elem {