retain files in Pure.thy, notably $POLYML_EXE;
authorwenzelm
Mon Nov 27 15:59:24 2017 +0100 (11 months ago)
changeset 67097d1b8464654c5
parent 67096 e77f13a6a501
child 67098 0f750a6dc754
retain files in Pure.thy, notably $POLYML_EXE;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Nov 27 11:45:20 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Nov 27 15:59:24 2017 +0100
     1.3 @@ -238,8 +238,9 @@
     1.4              val loaded_files =
     1.5                if (inlined_files) {
     1.6                  if (Sessions.is_pure(info.name)) {
     1.7 -                  (Thy_Header.PURE -> resources.pure_files(overall_syntax, info.dir)) ::
     1.8 -                    dependencies.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
     1.9 +                  val pure_files = resources.pure_files(overall_syntax, info.dir)
    1.10 +                  dependencies.loaded_files.map({ case (name, files) =>
    1.11 +                    (name, if (name == Thy_Header.PURE) pure_files ::: files else files) })
    1.12                  }
    1.13                  else dependencies.loaded_files
    1.14                }