# HG changeset patch
# User wenzelm
# Date 1491334431 -7200
# Node ID 4ad983094226b7152a21550c2cd7f420afce333c
# Parent  35a85aa725e99a60172b9e517a30a77be457ac78
proper base name;

diff -r 35a85aa725e9 -r 4ad983094226 src/Pure/Thy/present.scala
--- 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) =>