| changeset 59440 | 07e3c15cb10c |
| parent 59245 | be4180f3c236 |
| child 66823 | f529719cc47d |
| 59439:397ce0940c44 | 59440:07e3c15cb10c |
|---|---|
8 |
8 |
9 object Graph_Display |
9 object Graph_Display |
10 { |
10 { |
11 /* graph entries */ |
11 /* graph entries */ |
12 |
12 |
13 type Entry = ((String, (String, XML.Body)), List[String]) |
13 type Entry = ((String, (String, XML.Body)), List[String]) // ident, name, content, parents |
14 |
14 |
15 |
15 |
16 /* graph structure */ |
16 /* graph structure */ |
17 |
17 |
18 object Node |
18 object Node |