# HG changeset patch
# User wenzelm
# Date 1491647489 -7200
# Node ID 862bfd2b4fd41b2ce08e4ade9d8572c1638b84c8
# Parent  378175f4432812d494d31b146640a9c122f9f341
tuned signature;

diff -r 378175f44328 -r 862bfd2b4fd4 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Apr 07 21:17:18 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Sat Apr 08 12:31:29 2017 +0200
@@ -117,6 +117,8 @@
       def loaded_theory: Name = Name(theory, "", theory)
       def is_theory: Boolean = theory.nonEmpty
 
+      def theory_base_name: String = Long_Name.base_name(theory)
+
       override def toString: String = if (is_theory) theory else node
 
       def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
diff -r 378175f44328 -r 862bfd2b4fd4 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Apr 07 21:17:18 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sat Apr 08 12:31:29 2017 +0200
@@ -359,7 +359,7 @@
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
           { case Document.Node.Deps(header) =>
               val master_dir = File.standard_url(name.master_dir)
-              val theory = Long_Name.base_name(name.theory)
+              val theory = name.theory_base_name  // FIXME
               val imports = header.imports.map({ case (a, _) => a.node })
               val keywords =
                 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
diff -r 378175f44328 -r 862bfd2b4fd4 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Apr 07 21:17:18 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Sat Apr 08 12:31:29 2017 +0200
@@ -101,7 +101,7 @@
       try {
         val header = Thy_Header.read(reader, start, strict).decode_symbols
 
-        val base_name = Long_Name.base_name(node_name.theory)
+        val base_name = node_name.theory_base_name
         val (name, pos) = header.name
         if (base_name != name)
           error("Bad theory name " + quote(name) +
diff -r 378175f44328 -r 862bfd2b4fd4 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Fri Apr 07 21:17:18 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Sat Apr 08 12:31:29 2017 +0200
@@ -85,7 +85,7 @@
         case (loaded, dep) =>
           val name = dep.name.loaded_theory
           loaded + (name.theory -> name) +
-            (Long_Name.base_name(name.theory) -> name)  // legacy
+            (name.theory_base_name -> name)  // legacy
       }
 
     def loaded_files: List[Path] =
@@ -108,7 +108,7 @@
 
       def node(name: Document.Node.Name): Graph_Display.Node =
         if (parent_base.loaded_theory(name)) parent_session_node
-        else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory)
+        else Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
 
       (Graph_Display.empty_graph /: deps) {
         case (g, dep) =>