# HG changeset patch
# User wenzelm
# Date 1422202657 -3600
# Node ID 07e3c15cb10cd493998f7718bdb6a37a27c0576b
# Parent  397ce0940c441cf2c16811a86a81ba8666bf9d57
tuned comments;

diff -r 397ce0940c44 -r 07e3c15cb10c src/Pure/General/graph_display.scala
--- a/src/Pure/General/graph_display.scala	Sun Jan 25 15:40:28 2015 +0100
+++ b/src/Pure/General/graph_display.scala	Sun Jan 25 17:17:37 2015 +0100
@@ -10,7 +10,7 @@
 {
   /* graph entries */
 
-  type Entry = ((String, (String, XML.Body)), List[String])
+  type Entry = ((String, (String, XML.Body)), List[String])  // ident, name, content, parents
 
 
   /* graph structure */