src/Pure/Thy/present.scala
changeset 65376 4ad983094226
parent 65344 b99283eed13c
child 65377 6e47a27e3d43
equal deleted inserted replaced
65375:35a85aa725e9 65376:4ad983094226
    24     val parent_session_node =
    24     val parent_session_node =
    25       Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
    25       Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
    26 
    26 
    27     def node(name: Document.Node.Name): Graph_Display.Node =
    27     def node(name: Document.Node.Name): Graph_Display.Node =
    28       if (parent_loaded(name.theory)) parent_session_node
    28       if (parent_loaded(name.theory)) parent_session_node
    29       else Graph_Display.Node(name.theory, "theory." + name.theory)
    29       else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory)
    30 
    30 
    31     (Graph_Display.empty_graph /: deps) {
    31     (Graph_Display.empty_graph /: deps) {
    32       case (g, dep) =>
    32       case (g, dep) =>
    33         if (parent_loaded(dep.name.theory)) g
    33         if (parent_loaded(dep.name.theory)) g
    34         else {
    34         else {