src/Pure/PIDE/resources.scala
changeset 59695 a03e0561bdbf
parent 59694 d2bb4b5ed862
child 59705 740a0ca7e09b
     1.1 --- a/src/Pure/PIDE/resources.scala	Sat Mar 14 18:18:40 2015 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sat Mar 14 19:51:36 2015 +0100
     1.3 @@ -91,7 +91,7 @@
     1.4    {
     1.5      if (reader.source.length > 0) {
     1.6        try {
     1.7 -        val header = Thy_Header.read(reader).decode_symbols
     1.8 +        val header = Thy_Header.read(reader, node_name.node).decode_symbols
     1.9  
    1.10          val base_name = Long_Name.base_name(node_name.theory)
    1.11          val (name, pos) = header.name
    1.12 @@ -100,7 +100,7 @@
    1.13              " for theory " + quote(name) + Position.here(pos))
    1.14  
    1.15          val imports =
    1.16 -          header.imports.map({ case (s, _) => import_name(qualifier, node_name, s) })
    1.17 +          header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
    1.18          Document.Node.Header(imports, header.keywords, Nil)
    1.19        }
    1.20        catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }