src/Pure/PIDE/resources.scala
changeset 65372 b722ee40c26c
parent 65368 7fb5aad28f38
child 65373 905ed0102c69
     1.1 --- a/src/Pure/PIDE/resources.scala	Tue Apr 04 18:43:58 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Tue Apr 04 19:40:47 2017 +0200
     1.3 @@ -67,12 +67,16 @@
     1.4      }
     1.5      else Nil
     1.6  
     1.7 -  def init_name(global: Boolean, raw_path: Path): Document.Node.Name =
     1.8 +  def qualify(name: String): String =
     1.9 +    if (Long_Name.is_qualified(name)) error("Bad qualified theory name " + quote(name))
    1.10 +    else if (session_base.global_theories.contains(name)) name
    1.11 +    else Long_Name.qualify(session_name, name)
    1.12 +
    1.13 +  def init_name(raw_path: Path): Document.Node.Name =
    1.14    {
    1.15      val path = raw_path.expand
    1.16      val node = path.implode
    1.17 -    val qualifier = if (global) "" else session_name
    1.18 -    val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
    1.19 +    val theory = qualify(Thy_Header.thy_name(node).getOrElse(""))
    1.20      val master_dir = if (theory == "") "" else path.dir.implode
    1.21      Document.Node.Name(node, master_dir, theory)
    1.22    }