updated to polyml-test-1b2dcf8f5202;
authorwenzelm
Sun, 27 Jan 2019 17:30:09 +0100
changeset 69760 bb0a354f6b46
parent 69759 6a9a8ef5e4c6
child 69761 aec42cee2521
updated to polyml-test-1b2dcf8f5202;
Admin/components/components.sha1
Admin/components/main
Admin/polyml/README
src/Pure/Tools/build.scala
--- 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
--- 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
--- 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
--- 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)))