changeset 72775 | 0a94eb91190d |
parent 72774 | 51c0f79d6eed |
child 72778 | 83e581c9a5f1 |
--- a/src/Pure/PIDE/command.scala Sun Nov 29 15:33:19 2020 +0100 +++ b/src/Pure/PIDE/command.scala Sun Nov 29 15:41:36 2020 +0100 @@ -419,7 +419,7 @@ val imports_pos = header.imports_pos val raw_imports = try { - val read_imports = Thy_Header.read(reader).imports + val read_imports = Thy_Header.read(node_name, reader).imports if (imports_pos.length == read_imports.length) read_imports else error("") } catch { case _: Throwable => List.fill(imports_pos.length)("") }