proper base name;
authorwenzelm
Tue, 04 Apr 2017 21:33:51 +0200
changeset 65376 4ad983094226
parent 65375 35a85aa725e9
child 65377 6e47a27e3d43
proper base name;
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) =>