src/Pure/ML-Systems/ml_system.ML
changeset 60962 faa452d8e265
parent 48416 5787e1c911d0
child 60989 c967d423953a
equal deleted inserted replaced
60961:49d1ea25f1a4 60962:faa452d8e265
     9   val name: string
     9   val name: string
    10   val is_polyml: bool
    10   val is_polyml: bool
    11   val is_smlnj: bool
    11   val is_smlnj: bool
    12   val platform: string
    12   val platform: string
    13   val platform_is_cygwin: bool
    13   val platform_is_cygwin: bool
       
    14   val platform_is_windows: bool
    14   val share_common_data: unit -> unit
    15   val share_common_data: unit -> unit
    15   val save_state: string -> unit
    16   val save_state: string -> unit
    16 end;
    17 end;
    17 
    18 
    18 structure ML_System: ML_SYSTEM =
    19 structure ML_System: ML_SYSTEM =
    22 val is_polyml = String.isPrefix "polyml" name;
    23 val is_polyml = String.isPrefix "polyml" name;
    23 val is_smlnj = String.isPrefix "smlnj" name;
    24 val is_smlnj = String.isPrefix "smlnj" name;
    24 
    25 
    25 val SOME platform = OS.Process.getEnv "ML_PLATFORM";
    26 val SOME platform = OS.Process.getEnv "ML_PLATFORM";
    26 val platform_is_cygwin = String.isSuffix "cygwin" platform;
    27 val platform_is_cygwin = String.isSuffix "cygwin" platform;
       
    28 val platform_is_windows = String.isSuffix "windows" platform;
    27 
    29 
    28 fun share_common_data () = ();
    30 fun share_common_data () = ();
    29 fun save_state _ = raise Fail "Cannot save state -- undefined operation";
    31 fun save_state _ = raise Fail "Cannot save state -- undefined operation";
    30 
    32 
    31 end;
    33 end;