# HG changeset patch
# User wenzelm
# Date 1491328316 -7200
# Node ID 905ed0102c69ba716975c4a088fae44a680d57f0
# Parent  b722ee40c26c1a637e510cf6d096e62246e73869
clarified: allow to qualify theories from ROOT;

diff -r b722ee40c26c -r 905ed0102c69 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Apr 04 19:40:47 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Apr 04 19:51:56 2017 +0200
@@ -68,8 +68,7 @@
     else Nil
 
   def qualify(name: String): String =
-    if (Long_Name.is_qualified(name)) error("Bad qualified theory name " + quote(name))
-    else if (session_base.global_theories.contains(name)) name
+    if (session_base.global_theories.contains(name) || Long_Name.is_qualified(name)) name
     else Long_Name.qualify(session_name, name)
 
   def init_name(raw_path: Path): Document.Node.Name =
diff -r b722ee40c26c -r 905ed0102c69 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Apr 04 19:40:47 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Apr 04 19:51:56 2017 +0200
@@ -185,7 +185,12 @@
 
     def global_theories: List[String] =
       for { (global, _, paths) <- theories if global; path <- paths }
-      yield path.base.implode
+      yield {
+        val name = path.base.implode
+        if (Long_Name.is_qualified(name))
+          error("Bad qualified name for global theory " + quote(name))
+        else name
+      }
   }
 
   object Tree