author | wenzelm |
Tue, 04 Apr 2017 21:33:51 +0200 | |
changeset 65376 | 4ad983094226 |
parent 65375 | 35a85aa725e9 |
child 65377 | 6e47a27e3d43 |
--- a/src/Pure/Thy/present.scala Tue Apr 04 21:11:40 2017 +0200 +++ b/src/Pure/Thy/present.scala Tue Apr 04 21:33:51 2017 +0200 @@ -26,7 +26,7 @@ def node(name: Document.Node.Name): Graph_Display.Node = if (parent_loaded(name.theory)) parent_session_node - else Graph_Display.Node(name.theory, "theory." + name.theory) + else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory) (Graph_Display.empty_graph /: deps) { case (g, dep) =>