back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";
authorwenzelm
Tue Apr 04 16:18:53 2017 +0200 (2017-04-04)
changeset 653687fb5aad28f38
parent 65367 83c30e290702
child 65369 27c1b5e952bd
back to more liberal imports (amending 908a27a4b9c9): tolerate mixed situations like "GCD" vs. "~~/src/HOL/GCD";
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Tue Apr 04 15:05:00 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Tue Apr 04 16:18:53 2017 +0200
     1.3 @@ -80,15 +80,12 @@
     1.4    def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
     1.5    {
     1.6      val theory = Thy_Header.base_name(s)
     1.7 -    val is_base_name = Thy_Header.is_base_name(s)
     1.8 -    val is_qualified = is_base_name && Long_Name.is_qualified(s)
     1.9 +    val is_qualified = Thy_Header.is_base_name(s) && Long_Name.is_qualified(s)
    1.10  
    1.11      val known_theory =
    1.12 -      if (is_base_name)
    1.13 -        session_base.known_theories.get(theory) orElse
    1.14 -        (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
    1.15 -         else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
    1.16 -      else None
    1.17 +      session_base.known_theories.get(theory) orElse
    1.18 +      (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
    1.19 +       else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
    1.20  
    1.21      known_theory match {
    1.22        case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)