src/Pure/ML-Systems/ml_system.ML

--- 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;