# HG changeset patch
# User wenzelm
# Date 1459631648 -7200
# Node ID e6e80a8bf624bc120648c40b1321e17e76a69afe
# Parent  3498c66b5e5529cb9e62ed20ec9d077c3dc6b4c9
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;

diff -r 3498c66b5e55 -r e6e80a8bf624 src/Pure/ML/ml_heap.ML
--- a/src/Pure/ML/ml_heap.ML	Sat Apr 02 22:46:12 2016 +0200
+++ b/src/Pure/ML/ml_heap.ML	Sat Apr 02 23:14:08 2016 +0200
@@ -6,10 +6,19 @@
 
 signature ML_HEAP =
 sig
+  val obj_size: 'a -> int
   val share_common_data: unit -> unit
+  val save_child: string -> unit
 end;
 
 structure ML_Heap: ML_HEAP =
 struct
-  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+
+val obj_size = PolyML.objSize;
+
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+
+fun save_child name =
+  PolyML.SaveState.saveChild (name, List.length (PolyML.SaveState.showHierarchy ()));
+
 end;
diff -r 3498c66b5e55 -r e6e80a8bf624 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Apr 02 22:46:12 2016 +0200
+++ b/src/Pure/ROOT.ML	Sat Apr 02 23:14:08 2016 +0200
@@ -346,3 +346,5 @@
 val use_thy = use_thys o single;
 
 Proofterm.proofs := 0;
+
+structure PolyML = struct structure IntInf = PolyML.IntInf end;
diff -r 3498c66b5e55 -r e6e80a8bf624 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Apr 02 22:46:12 2016 +0200
+++ b/src/Pure/Tools/build.scala	Sat Apr 02 23:14:08 2016 +0200
@@ -235,9 +235,7 @@
     val output = store.output_dir + Path.basic(name)
     def output_path: Option[Path] = if (do_output) Some(output) else None
     def output_save_state: String =
-      if (do_output)
-        "PolyML.SaveState.saveChild (" + ML_Syntax.print_string0(File.platform_path(output)) +
-          ", List.length (PolyML.SaveState.showHierarchy ()))"
+      if (do_output) "ML_Heap.save_child " + ML_Syntax.print_string0(File.platform_path(output))
       else ""
     output.file.delete