# HG changeset patch # User wenzelm # Date 1511794764 -3600 # Node ID d1b8464654c5ba814a5ef6380bc0426df494b30f # Parent e77f13a6a50107ddb51bc5e3e7eb1bd3ded17791 retain files in Pure.thy, notably $POLYML_EXE; diff -r e77f13a6a501 -r d1b8464654c5 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Mon Nov 27 11:45:20 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Mon Nov 27 15:59:24 2017 +0100 @@ -238,8 +238,9 @@ val loaded_files = if (inlined_files) { if (Sessions.is_pure(info.name)) { - (Thy_Header.PURE -> resources.pure_files(overall_syntax, info.dir)) :: - dependencies.loaded_files.filterNot(p => p._1 == Thy_Header.PURE) + val pure_files = resources.pure_files(overall_syntax, info.dir) + dependencies.loaded_files.map({ case (name, files) => + (name, if (name == Thy_Header.PURE) pure_files ::: files else files) }) } else dependencies.loaded_files }