src/Pure/PIDE/resources.scala
changeset 65392 f365f61f2081
parent 65373 905ed0102c69
child 65408 c728f922f657
     1.1 --- a/src/Pure/PIDE/resources.scala	Wed Apr 05 11:39:36 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Wed Apr 05 22:00:44 2017 +0200
     1.3 @@ -67,38 +67,27 @@
     1.4      }
     1.5      else Nil
     1.6  
     1.7 -  def qualify(name: String): String =
     1.8 -    if (session_base.global_theories.contains(name) || Long_Name.is_qualified(name)) name
     1.9 -    else Long_Name.qualify(session_name, name)
    1.10 -
    1.11 -  def init_name(raw_path: Path): Document.Node.Name =
    1.12 +  def import_name(dir: String, s: String): Document.Node.Name =
    1.13    {
    1.14 -    val path = raw_path.expand
    1.15 -    val node = path.implode
    1.16 -    val theory = qualify(Thy_Header.thy_name(node).getOrElse(""))
    1.17 -    val master_dir = if (theory == "") "" else path.dir.implode
    1.18 -    Document.Node.Name(node, master_dir, theory)
    1.19 -  }
    1.20 -
    1.21 -  def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
    1.22 -  {
    1.23 -    val theory = Thy_Header.base_name(s)
    1.24 -    val is_qualified = Thy_Header.is_base_name(s) && Long_Name.is_qualified(s)
    1.25 +    val thy = Thy_Header.base_name(s)
    1.26 +    val is_global = session_base.global_theories.contains(thy)
    1.27 +    val is_qualified = Long_Name.is_qualified(thy)
    1.28  
    1.29      val known_theory =
    1.30 -      session_base.known_theories.get(theory) orElse
    1.31 -      (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
    1.32 -       else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
    1.33 +      session_base.known_theories.get(thy) orElse
    1.34 +      (if (is_global) None
    1.35 +       else if (is_qualified) session_base.known_theories.get(Long_Name.base_name(thy))
    1.36 +       else session_base.known_theories.get(Long_Name.qualify(session_name, thy)))
    1.37  
    1.38      known_theory match {
    1.39        case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
    1.40        case Some(name) => name
    1.41 -      case None if is_qualified => Document.Node.Name.theory(theory)
    1.42        case None =>
    1.43          val path = Path.explode(s)
    1.44 -        val node = append(master.master_dir, thy_path(path))
    1.45 -        val master_dir = append(master.master_dir, path.dir)
    1.46 -        Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory))
    1.47 +        val node = append(dir, thy_path(path))
    1.48 +        val master_dir = append(dir, path.dir)
    1.49 +        val theory = if (is_global || is_qualified) thy else Long_Name.qualify(session_name, thy)
    1.50 +        Document.Node.Name(node, master_dir, theory)
    1.51      }
    1.52    }
    1.53  
    1.54 @@ -126,7 +115,7 @@
    1.55              Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
    1.56  
    1.57          val imports =
    1.58 -          header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
    1.59 +          header.imports.map({ case (s, pos) => (import_name(node_name.master_dir, s), pos) })
    1.60          Document.Node.Header(imports, header.keywords, header.abbrevs)
    1.61        }
    1.62        catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
    1.63 @@ -143,9 +132,11 @@
    1.64  
    1.65    def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
    1.66      if (Thy_Header.is_ml_root(name.theory))
    1.67 -      Some(Document.Node.Header(List((import_name(name, Thy_Header.ML_BOOTSTRAP), Position.none))))
    1.68 +      Some(Document.Node.Header(
    1.69 +        List((import_name(name.master_dir, Thy_Header.ML_BOOTSTRAP), Position.none))))
    1.70      else if (Thy_Header.is_bootstrap(name.theory))
    1.71 -      Some(Document.Node.Header(List((import_name(name, Thy_Header.PURE), Position.none))))
    1.72 +      Some(Document.Node.Header(
    1.73 +        List((import_name(name.master_dir, Thy_Header.PURE), Position.none))))
    1.74      else None
    1.75  
    1.76