diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/PIDE/xml.scala
--- 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
   {