src/Pure/PIDE/document.ML
2010-08-05 ago simplified/refined document model: collection of named nodes, without proper dependencies yet;