src/Pure/ML-Systems/ml_system.ML
author wenzelm
Fri Apr 12 14:54:14 2013 +0200 (2013-04-12)
changeset 51700 c8f2bad67dbb
parent 48416 5787e1c911d0
child 60962 faa452d8e265
permissions -rw-r--r--
tuned signature;
tuned comments;
     1 (*  Title:      Pure/ML-Systems/ml_system.ML
     2     Author:     Makarius
     3 
     4 ML system and platform operations.
     5 *)
     6 
     7 signature ML_SYSTEM =
     8 sig
     9   val name: string
    10   val is_polyml: bool
    11   val is_smlnj: bool
    12   val platform: string
    13   val platform_is_cygwin: bool
    14   val share_common_data: unit -> unit
    15   val save_state: string -> unit
    16 end;
    17 
    18 structure ML_System: ML_SYSTEM =
    19 struct
    20 
    21 val SOME name = OS.Process.getEnv "ML_SYSTEM";
    22 val is_polyml = String.isPrefix "polyml" name;
    23 val is_smlnj = String.isPrefix "smlnj" name;
    24 
    25 val SOME platform = OS.Process.getEnv "ML_PLATFORM";
    26 val platform_is_cygwin = String.isSuffix "cygwin" platform;
    27 
    28 fun share_common_data () = ();
    29 fun save_state _ = raise Fail "Cannot save state -- undefined operation";
    30 
    31 end;
    32