more ML_System operations;

--- a/src/Pure/ML-Systems/ml_system.ML	Sat Jul 21 10:55:42 2012 +0200
+++ b/src/Pure/ML-Systems/ml_system.ML	Sat Jul 21 12:42:28 2012 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML-Systems/ml_system.ML
     Author:     Makarius
 
-ML system and platform information.
+ML system and platform operations.
 *)
 
 signature ML_SYSTEM =
@@ -11,6 +11,8 @@
   val is_smlnj: bool
   val platform: string
   val platform_is_cygwin: bool
+  val share_common_data: unit -> unit
+  val save_state: string -> unit
 end;
 
 structure ML_System: ML_SYSTEM =
@@ -23,5 +25,8 @@
 val SOME platform = OS.Process.getEnv "ML_PLATFORM";
 val platform_is_cygwin = String.isSuffix "cygwin" platform;
 
+fun share_common_data () = ();
+fun save_state _ = raise Fail "Cannot save state -- undefined operation";
+
 end;
 

--- a/src/Pure/ML-Systems/polyml.ML	Sat Jul 21 10:55:42 2012 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Sat Jul 21 12:42:28 2012 +0200
@@ -70,10 +70,20 @@
 fun quit () = exit 0;
 
 
-(* ML system identification *)
+(* ML system operations *)
 
 use "ML-Systems/ml_system.ML";
 
+structure ML_System =
+struct
+
+open ML_System;
+
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+val save_state = PolyML.SaveState.saveState;
+
+end;
+
 
 (* ML runtime system *)
 
@@ -91,8 +101,6 @@
 
 val pointer_eq = PolyML.pointerEq;
 
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
 
 (* ML compiler *)
 

--- a/src/Pure/ML-Systems/smlnj.ML	Sat Jul 21 10:55:42 2012 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Sat Jul 21 12:42:28 2012 +0200
@@ -29,8 +29,6 @@
 CM.autoload "$smlnj/init/init.cmi";
 val pointer_eq = InlineT.ptreql;
 
-fun share_common_data () = ();
-
 
 (* restore old-style character / string functions *)
 
@@ -162,5 +160,19 @@
 
 use "ML-Systems/unsynchronized.ML";
 
+
+(* ML system operations *)
+
 use "ML-Systems/ml_system.ML";
 
+structure ML_System =
+struct
+
+open ML_System;
+
+fun save_state name =
+  if SMLofNJ.exportML name then ()
+  else OS.FileSys.rename {old = name ^ "." ^ platform, new = name};
+
+end;
+