src/Pure/PIDE/command.scala
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)("") }