src/Pure/PIDE/resources.scala
changeset 65445 e9e7f5f5794c
parent 65441 9425e4d8bdb6
child 65452 9e9750a7932c
     1.1 --- a/src/Pure/PIDE/resources.scala	Sat Apr 08 21:35:04 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sat Apr 08 22:36:32 2017 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  class Resources(
     1.6    val session_base: Sessions.Base,
     1.7 -  val default_qualifier: String = "",
     1.8 +  val default_qualifier: String = Sessions.DRAFT,
     1.9    val log: Logger = No_Logger)
    1.10  {
    1.11    val thy_info = new Thy_Info(this)
    1.12 @@ -67,12 +67,16 @@
    1.13      }
    1.14      else Nil
    1.15  
    1.16 -  def import_name(dir: String, s: String): Document.Node.Name =
    1.17 +  def theory_qualifier(name: Document.Node.Name): String =
    1.18 +    Long_Name.qualifier(name.theory)
    1.19 +
    1.20 +  def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
    1.21    {
    1.22      val theory0 = Thy_Header.base_name(s)
    1.23      val theory =
    1.24 -      if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
    1.25 -      else Long_Name.qualify(default_qualifier, theory0)
    1.26 +      if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)
    1.27 +        || true /* FIXME */) theory0
    1.28 +      else theory0 // FIXME Long_Name.qualify(qualifier, theory0)
    1.29  
    1.30      session_base.loaded_theories.get(theory) orElse
    1.31      session_base.loaded_theories.get(theory0) orElse
    1.32 @@ -109,7 +113,8 @@
    1.33              Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
    1.34  
    1.35          val imports =
    1.36 -          header.imports.map({ case (s, pos) => (import_name(node_name.master_dir, s), pos) })
    1.37 +          header.imports.map({ case (s, pos) =>
    1.38 +            (import_name(theory_qualifier(node_name), node_name.master_dir, s), pos) })
    1.39          Document.Node.Header(imports, header.keywords, header.abbrevs)
    1.40        }
    1.41        catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
    1.42 @@ -125,13 +130,20 @@
    1.43    /* special header */
    1.44  
    1.45    def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
    1.46 -    if (Thy_Header.is_ml_root(name.theory))
    1.47 -      Some(Document.Node.Header(
    1.48 -        List((import_name(name.master_dir, Thy_Header.ML_BOOTSTRAP), Position.none))))
    1.49 -    else if (Thy_Header.is_bootstrap(name.theory))
    1.50 -      Some(Document.Node.Header(
    1.51 -        List((import_name(name.master_dir, Thy_Header.PURE), Position.none))))
    1.52 -    else None
    1.53 +  {
    1.54 +    val qualifier = theory_qualifier(name)
    1.55 +    val dir = name.master_dir
    1.56 +
    1.57 +    val imports =
    1.58 +      if (Thy_Header.is_ml_root(name.theory))
    1.59 +        List(import_name(qualifier, dir, Thy_Header.ML_BOOTSTRAP))
    1.60 +      else if (Thy_Header.is_bootstrap(name.theory))
    1.61 +        List(import_name(qualifier, dir, Thy_Header.PURE))
    1.62 +      else Nil
    1.63 +
    1.64 +    if (imports.isEmpty) None
    1.65 +    else Some(Document.Node.Header(imports.map((_, Position.none))))
    1.66 +  }
    1.67  
    1.68  
    1.69    /* blobs */