--- a/src/Pure/General/multi_map.scala Sat Apr 26 13:07:20 2014 +0200
+++ b/src/Pure/General/multi_map.scala Sat Apr 26 13:18:46 2014 +0200
@@ -1,5 +1,6 @@
/* Title: Pure/General/multi_map.scala
Module: PIDE
+ Author: Makarius
Maps with multiple entries per key.
*/
--- a/src/Pure/General/word.scala Sat Apr 26 13:07:20 2014 +0200
+++ b/src/Pure/General/word.scala Sat Apr 26 13:18:46 2014 +0200
@@ -1,5 +1,4 @@
/* Title: Pure/General/word.scala
- Module: PIDE
Author: Makarius
Support for plain text words.
--- a/src/Pure/PIDE/document_id.scala Sat Apr 26 13:07:20 2014 +0200
+++ b/src/Pure/PIDE/document_id.scala Sat Apr 26 13:18:46 2014 +0200
@@ -1,4 +1,5 @@
/* Title: Pure/PIDE/document_id.scala
+ Module: PIDE
Author: Makarius
Unique identifiers for document structure.