# HG changeset patch # User wenzelm # Date 1548606609 -3600 # Node ID bb0a354f6b462bb29530a71958775296aeacaa8b # Parent 6a9a8ef5e4c604f5215323ce29ae9fbfa6a01a87 updated to polyml-test-1b2dcf8f5202; diff -r 6a9a8ef5e4c6 -r bb0a354f6b46 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Fri Jan 25 22:13:48 2019 +0000 +++ b/Admin/components/components.sha1 Sun Jan 27 17:30:09 2019 +0100 @@ -195,6 +195,7 @@ 171b5783b88522a35e4822b19ef8ba838c04f494 polyml-5.7.1.tar.gz 5fbcab1da2b5eb97f24da2590ece189d55b3a105 polyml-5.7.tar.gz 49f1adfacdd6d29fa9f72035d94a31eaac411a97 polyml-test-0a6ebca445fc.tar.gz +a0064c157a59e2706e18512a49a6dca914fa17fc polyml-test-1b2dcf8f5202.tar.gz 4e6543dbbb2b2aa402fd61428e1c045c48f18b47 polyml-test-79534495ee94.tar.gz 853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz c629cd499a724bbe37b962f727e4ff340c50299d polyml-test-8529546198aa.tar.gz diff -r 6a9a8ef5e4c6 -r bb0a354f6b46 Admin/components/main --- a/Admin/components/main Fri Jan 25 22:13:48 2019 +0000 +++ b/Admin/components/main Sun Jan 27 17:30:09 2019 +0100 @@ -12,7 +12,7 @@ kodkodi-1.5.2-1 nunchaku-0.5 opam-1.2.2 -polyml-test-a444f281ccec +polyml-test-1b2dcf8f5202 postgresql-42.2.5 scala-2.12.8 smbc-0.4.1 diff -r 6a9a8ef5e4c6 -r bb0a354f6b46 Admin/polyml/README --- a/Admin/polyml/README Fri Jan 25 22:13:48 2019 +0000 +++ b/Admin/polyml/README Sun Jan 27 17:30:09 2019 +0100 @@ -3,7 +3,7 @@ This compilation of Poly/ML (https://www.polyml.org) is based on the repository version -https://github.com/polyml/polyml/commit/a444f281ccec (master). +https://github.com/polyml/polyml/commit/1b2dcf8f5202 (master). The Isabelle repository provides the administrative tool "build_polyml", which can be used in the polyml component directory as @@ -48,4 +48,4 @@ Makarius - 23-Jan-2019 + 27-Jan-2019 diff -r 6a9a8ef5e4c6 -r bb0a354f6b46 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Jan 25 22:13:48 2019 +0000 +++ b/src/Pure/Tools/build.scala Sun Jan 27 17:30:09 2019 +0100 @@ -233,7 +233,8 @@ ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString) def save_heap: String = - (if (info.theories.isEmpty) "" else "ML_Heap.share_common_data (); ") + + (if (info.theories.isEmpty) "" + else """cond_timeit true "share_common_data" ML_Heap.share_common_data; """) + "ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name)))