structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
authorwenzelm
Sat Apr 02 23:14:08 2016 +0200 (2016-04-02 ago)
changeset 62825e6e80a8bf624
parent 62824 3498c66b5e55
child 62826 eb94e570c1a4
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
src/Pure/ML/ml_heap.ML
src/Pure/ROOT.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/ML/ml_heap.ML	Sat Apr 02 22:46:12 2016 +0200
     1.2 +++ b/src/Pure/ML/ml_heap.ML	Sat Apr 02 23:14:08 2016 +0200
     1.3 @@ -6,10 +6,19 @@
     1.4  
     1.5  signature ML_HEAP =
     1.6  sig
     1.7 +  val obj_size: 'a -> int
     1.8    val share_common_data: unit -> unit
     1.9 +  val save_child: string -> unit
    1.10  end;
    1.11  
    1.12  structure ML_Heap: ML_HEAP =
    1.13  struct
    1.14 -  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
    1.15 +
    1.16 +val obj_size = PolyML.objSize;
    1.17 +
    1.18 +fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
    1.19 +
    1.20 +fun save_child name =
    1.21 +  PolyML.SaveState.saveChild (name, List.length (PolyML.SaveState.showHierarchy ()));
    1.22 +
    1.23  end;
     2.1 --- a/src/Pure/ROOT.ML	Sat Apr 02 22:46:12 2016 +0200
     2.2 +++ b/src/Pure/ROOT.ML	Sat Apr 02 23:14:08 2016 +0200
     2.3 @@ -346,3 +346,5 @@
     2.4  val use_thy = use_thys o single;
     2.5  
     2.6  Proofterm.proofs := 0;
     2.7 +
     2.8 +structure PolyML = struct structure IntInf = PolyML.IntInf end;
     3.1 --- a/src/Pure/Tools/build.scala	Sat Apr 02 22:46:12 2016 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Sat Apr 02 23:14:08 2016 +0200
     3.3 @@ -235,9 +235,7 @@
     3.4      val output = store.output_dir + Path.basic(name)
     3.5      def output_path: Option[Path] = if (do_output) Some(output) else None
     3.6      def output_save_state: String =
     3.7 -      if (do_output)
     3.8 -        "PolyML.SaveState.saveChild (" + ML_Syntax.print_string0(File.platform_path(output)) +
     3.9 -          ", List.length (PolyML.SaveState.showHierarchy ()))"
    3.10 +      if (do_output) "ML_Heap.save_child " + ML_Syntax.print_string0(File.platform_path(output))
    3.11        else ""
    3.12      output.file.delete
    3.13