src/Pure/General/graph_display.scala
changeset 59440 07e3c15cb10c
parent 59245 be4180f3c236
child 66823 f529719cc47d
equal deleted inserted replaced
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