clarified ML heap operations;

--- a/src/Pure/PIDE/protocol.ML	Mon Feb 29 15:06:53 2016 +0100
+++ b/src/Pure/PIDE/protocol.ML	Mon Feb 29 15:23:13 2016 +0100
@@ -123,8 +123,8 @@
         handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
 
 val _ =
-  Isabelle_Process.protocol_command "ML_System.share_common_data"
-    (fn [] => ML_System.share_common_data ());
+  Isabelle_Process.protocol_command "ML_Heap.share_common_data"
+    (fn [] => ML_Heap.share_common_data ());
 
 end;
 

--- a/src/Pure/PIDE/session.ML	Mon Feb 29 15:06:53 2016 +0100
+++ b/src/Pure/PIDE/session.ML	Mon Feb 29 15:23:13 2016 +0100
@@ -77,8 +77,8 @@
 
 fun save heap =
  (shutdown ();
-  ML_System.share_common_data ();
-  ML_System.save_state heap);
+  ML_Heap.share_common_data ();
+  ML_Heap.save_state heap);
 
 
 

--- a/src/Pure/RAW/ROOT_polyml.ML	Mon Feb 29 15:06:53 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Mon Feb 29 15:23:13 2016 +0100
@@ -29,23 +29,16 @@
 end;
 
 
-(* ML system operations *)
-
-if ML_System.name = "polyml-5.3.0"
-then use "RAW/share_common_data_polyml-5.3.0.ML"
-else ();
+(* ML heap operations *)
 
 fun ml_platform_path (s: string) = s;
 fun ml_standard_path (s: string) = s;
 
 if ML_System.platform_is_windows then use "RAW/windows_path.ML" else ();
 
-structure ML_System =
-struct
-  open ML_System;
-  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-  val save_state = PolyML.SaveState.saveState o ml_platform_path;
-end;
+if ML_System.name = "polyml-5.3.0"
+then use "RAW/ml_heap_polyml-5.3.0.ML"
+else use "RAW/ml_heap.ML";
 
 
 (* exceptions *)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_heap.ML	Mon Feb 29 15:23:13 2016 +0100
@@ -0,0 +1,17 @@
+(*  Title:      Pure/RAW/ml_heap.ML
+    Author:     Makarius
+
+ML heap operations.
+*)
+
+signature ML_HEAP =
+sig
+  val share_common_data: unit -> unit
+  val save_state: string -> unit
+end;
+
+structure ML_Heap: ML_HEAP =
+struct
+  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+  val save_state = PolyML.SaveState.saveState o ml_platform_path;
+end;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/ml_heap_polyml-5.3.0.ML	Mon Feb 29 15:23:13 2016 +0100
@@ -0,0 +1,17 @@
+(*  Title:      Pure/RAW/ml_heap.ML
+    Author:     Makarius
+
+ML heap operations.
+*)
+
+signature ML_HEAP =
+sig
+  val share_common_data: unit -> unit
+  val save_state: string -> unit
+end;
+
+structure ML_Heap: ML_HEAP =
+struct
+  fun share_common_data () = ();
+  val save_state = PolyML.SaveState.saveState o ml_platform_path;
+end;

--- a/src/Pure/RAW/ml_system.ML	Mon Feb 29 15:06:53 2016 +0100
+++ b/src/Pure/RAW/ml_system.ML	Mon Feb 29 15:23:13 2016 +0100
@@ -9,20 +9,13 @@
   val name: string
   val platform: string
   val platform_is_windows: bool
-  val share_common_data: unit -> unit
-  val save_state: string -> unit
 end;
 
 structure ML_System: ML_SYSTEM =
 struct
 
 val SOME name = OS.Process.getEnv "ML_SYSTEM";
-
 val SOME platform = OS.Process.getEnv "ML_PLATFORM";
 val platform_is_windows = String.isSuffix "windows" platform;
 
-fun share_common_data () = ();
-fun save_state _ = raise Fail "Cannot save state -- undefined operation";
-
 end;
-

--- a/src/Pure/RAW/share_common_data_polyml-5.3.0.ML	Mon Feb 29 15:06:53 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(*  Title:      Pure/RAW/share_common_data_polyml-5.3.0.ML
-
-Dummy for Poly/ML 5.3.0, which cannot share the massive heap of HOL
-anymore.
-*)
-
-structure PolyML =
-struct
-  open PolyML;
-  fun shareCommonData _ = ();
-end;

--- a/src/Pure/ROOT	Mon Feb 29 15:06:53 2016 +0100
+++ b/src/Pure/ROOT	Mon Feb 29 15:23:13 2016 +0100
@@ -14,6 +14,8 @@
     "RAW/ml_compiler_parameters_polyml-5.6.ML"
     "RAW/ml_debugger.ML"
     "RAW/ml_debugger_polyml-5.6.ML"
+    "RAW/ml_heap.ML"
+    "RAW/ml_heap_polyml-5.3.0.ML"
     "RAW/ml_name_space_polyml-5.6.ML"
     "RAW/ml_name_space_polyml.ML"
     "RAW/ml_parse_tree.ML"
@@ -26,7 +28,6 @@
     "RAW/ml_stack_polyml-5.6.ML"
     "RAW/ml_system.ML"
     "RAW/multithreading.ML"
-    "RAW/share_common_data_polyml-5.3.0.ML"
     "RAW/single_assignment_polyml.ML"
     "RAW/unsynchronized.ML"
     "RAW/use_context.ML"
@@ -46,6 +47,8 @@
     "RAW/ml_compiler_parameters_polyml-5.6.ML"
     "RAW/ml_debugger.ML"
     "RAW/ml_debugger_polyml-5.6.ML"
+    "RAW/ml_heap.ML"
+    "RAW/ml_heap_polyml-5.3.0.ML"
     "RAW/ml_name_space_polyml-5.6.ML"
     "RAW/ml_name_space_polyml.ML"
     "RAW/ml_parse_tree.ML"
@@ -58,7 +61,6 @@
     "RAW/ml_stack_polyml-5.6.ML"
     "RAW/ml_system.ML"
     "RAW/multithreading.ML"
-    "RAW/share_common_data_polyml-5.3.0.ML"
     "RAW/single_assignment_polyml.ML"
     "RAW/unsynchronized.ML"
     "RAW/use_context.ML"