src/Pure/PIDE/resources.scala
changeset 65489 f3076367f4a8
parent 65488 331f09d9535e
child 65494 88e6442c3150
     1.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 17 12:20:45 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 17 12:29:50 2017 +0200
     1.3 @@ -93,6 +93,9 @@
     1.4          }
     1.5      }
     1.6  
     1.7 +  def import_name(node_name: Document.Node.Name, s: String): Document.Node.Name =
     1.8 +    import_name(theory_qualifier(node_name), node_name.master_dir, s)
     1.9 +
    1.10    def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.11    {
    1.12      val path = Path.explode(name.node)
    1.13 @@ -116,9 +119,7 @@
    1.14              " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
    1.15              Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
    1.16  
    1.17 -        val imports =
    1.18 -          header.imports.map({ case (s, pos) =>
    1.19 -            (import_name(theory_qualifier(node_name), node_name.master_dir, s), pos) })
    1.20 +        val imports = header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
    1.21          Document.Node.Header(imports, header.keywords, header.abbrevs)
    1.22        }
    1.23        catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
    1.24 @@ -135,16 +136,10 @@
    1.25  
    1.26    def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
    1.27    {
    1.28 -    val qualifier = theory_qualifier(name)
    1.29 -    val dir = name.master_dir
    1.30 -
    1.31      val imports =
    1.32 -      if (Thy_Header.is_ml_root(name.theory))
    1.33 -        List(import_name(qualifier, dir, Thy_Header.ML_BOOTSTRAP))
    1.34 -      else if (Thy_Header.is_bootstrap(name.theory))
    1.35 -        List(import_name(qualifier, dir, Thy_Header.PURE))
    1.36 +      if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
    1.37 +      else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE))
    1.38        else Nil
    1.39 -
    1.40      if (imports.isEmpty) None
    1.41      else Some(Document.Node.Header(imports.map((_, Position.none))))
    1.42    }