1.1 --- a/src/Pure/ML-Systems/ml_system.ML	Sat Jul 21 10:55:42 2012 +0200
     1.2 +++ b/src/Pure/ML-Systems/ml_system.ML	Sat Jul 21 12:42:28 2012 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/ML-Systems/ml_system.ML
     1.5      Author:     Makarius
     1.6  
     1.7 -ML system and platform information.
     1.8 +ML system and platform operations.
     1.9  *)
    1.10  
    1.11  signature ML_SYSTEM =
    1.12 @@ -11,6 +11,8 @@
    1.13    val is_smlnj: bool
    1.14    val platform: string
    1.15    val platform_is_cygwin: bool
    1.16 +  val share_common_data: unit -> unit
    1.17 +  val save_state: string -> unit
    1.18  end;
    1.19  
    1.20  structure ML_System: ML_SYSTEM =
    1.21 @@ -23,5 +25,8 @@
    1.22  val SOME platform = OS.Process.getEnv "ML_PLATFORM";
    1.23  val platform_is_cygwin = String.isSuffix "cygwin" platform;
    1.24  
    1.25 +fun share_common_data () = ();
    1.26 +fun save_state _ = raise Fail "Cannot save state -- undefined operation";
    1.27 +
    1.28  end;
    1.29  

     2.1 --- a/src/Pure/ML-Systems/polyml.ML	Sat Jul 21 10:55:42 2012 +0200
     2.2 +++ b/src/Pure/ML-Systems/polyml.ML	Sat Jul 21 12:42:28 2012 +0200
     2.3 @@ -70,10 +70,20 @@
     2.4  fun quit () = exit 0;
     2.5  
     2.6  
     2.7 -(* ML system identification *)
     2.8 +(* ML system operations *)
     2.9  
    2.10  use "ML-Systems/ml_system.ML";
    2.11  
    2.12 +structure ML_System =
    2.13 +struct
    2.14 +
    2.15 +open ML_System;
    2.16 +
    2.17 +fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
    2.18 +val save_state = PolyML.SaveState.saveState;
    2.19 +
    2.20 +end;
    2.21 +
    2.22  
    2.23  (* ML runtime system *)
    2.24  
    2.25 @@ -91,8 +101,6 @@
    2.26  
    2.27  val pointer_eq = PolyML.pointerEq;
    2.28  
    2.29 -fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
    2.30 -
    2.31  
    2.32  (* ML compiler *)
    2.33  

     3.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sat Jul 21 10:55:42 2012 +0200
     3.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sat Jul 21 12:42:28 2012 +0200
     3.3 @@ -29,8 +29,6 @@
     3.4  CM.autoload "$smlnj/init/init.cmi";
     3.5  val pointer_eq = InlineT.ptreql;
     3.6  
     3.7 -fun share_common_data () = ();
     3.8 -
     3.9  
    3.10  (* restore old-style character / string functions *)
    3.11  
    3.12 @@ -162,5 +160,19 @@
    3.13  
    3.14  use "ML-Systems/unsynchronized.ML";
    3.15  
    3.16 +
    3.17 +(* ML system operations *)
    3.18 +
    3.19  use "ML-Systems/ml_system.ML";
    3.20  
    3.21 +structure ML_System =
    3.22 +struct
    3.23 +
    3.24 +open ML_System;
    3.25 +
    3.26 +fun save_state name =
    3.27 +  if SMLofNJ.exportML name then ()
    3.28 +  else OS.FileSys.rename {old = name ^ "." ^ platform, new = name};
    3.29 +
    3.30 +end;
    3.31 +