diff -r d83797ef0d2d -r 546d78f0d81f src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Mon Nov 28 22:05:32 2011 +0100 +++ b/src/Pure/PIDE/xml.scala Mon Nov 28 22:18:19 2011 +0100 @@ -1,4 +1,5 @@ /* Title: Pure/PIDE/xml.scala + Module: Library Author: Makarius Untyped XML trees and basic data representation.