src/Pure/ML-Systems/ml_system.ML
author wenzelm
Sun, 09 Oct 2011 16:47:58 +0200
changeset 45107 76fef3e57004
parent 43948 8f5add916a99
child 48416 5787e1c911d0
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43948
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/ml_system.ML
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
     3
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
     4
ML system and platform information.
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
     5
*)
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
     6
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
     7
signature ML_SYSTEM =
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
     8
sig
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
     9
  val name: string
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    10
  val is_polyml: bool
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    11
  val is_smlnj: bool
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    12
  val platform: string
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    13
  val platform_is_cygwin: bool
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    14
end;
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    15
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    16
structure ML_System: ML_SYSTEM =
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    17
struct
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    18
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    19
val SOME name = OS.Process.getEnv "ML_SYSTEM";
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    20
val is_polyml = String.isPrefix "polyml" name;
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    21
val is_smlnj = String.isPrefix "smlnj" name;
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    22
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    23
val SOME platform = OS.Process.getEnv "ML_PLATFORM";
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    24
val platform_is_cygwin = String.isSuffix "cygwin" platform;
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    25
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    26
end;
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    27