tuned comments;
authorwenzelm
Sun, 25 Jan 2015 17:17:37 +0100
changeset 59440 07e3c15cb10c
parent 59439 397ce0940c44
child 59441 ab2c3597f1d3
tuned comments;
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 */