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