clarified: allow to qualify theories from ROOT;
authorwenzelm
Tue Apr 04 19:51:56 2017 +0200 (2017-04-04)
changeset 65373905ed0102c69
parent 65372 b722ee40c26c
child 65374 a5b38d8d3c1e
clarified: allow to qualify theories from ROOT;
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Tue Apr 04 19:40:47 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Tue Apr 04 19:51:56 2017 +0200
     1.3 @@ -68,8 +68,7 @@
     1.4      else Nil
     1.5  
     1.6    def qualify(name: String): String =
     1.7 -    if (Long_Name.is_qualified(name)) error("Bad qualified theory name " + quote(name))
     1.8 -    else if (session_base.global_theories.contains(name)) name
     1.9 +    if (session_base.global_theories.contains(name) || Long_Name.is_qualified(name)) name
    1.10      else Long_Name.qualify(session_name, name)
    1.11  
    1.12    def init_name(raw_path: Path): Document.Node.Name =
     2.1 --- a/src/Pure/Thy/sessions.scala	Tue Apr 04 19:40:47 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Tue Apr 04 19:51:56 2017 +0200
     2.3 @@ -185,7 +185,12 @@
     2.4  
     2.5      def global_theories: List[String] =
     2.6        for { (global, _, paths) <- theories if global; path <- paths }
     2.7 -      yield path.base.implode
     2.8 +      yield {
     2.9 +        val name = path.base.implode
    2.10 +        if (Long_Name.is_qualified(name))
    2.11 +          error("Bad qualified name for global theory " + quote(name))
    2.12 +        else name
    2.13 +      }
    2.14    }
    2.15  
    2.16    object Tree