--- a/src/Pure/PIDE/xml.scala Mon Oct 24 12:01:36 2016 +0200 +++ b/src/Pure/PIDE/xml.scala Mon Oct 24 12:16:12 2016 +0200 @@ -1,5 +1,4 @@ /* Title: Pure/PIDE/xml.scala - Module: PIDE Author: Makarius Untyped XML trees and basic data representation.