src/Pure/ML-Systems/ml_system.ML
author wenzelm
Sat, 24 Nov 2012 16:13:21 +0100
changeset 50185 820673500454
parent 48416 5787e1c911d0
child 60962 faa452d8e265
permissions -rw-r--r--
avoid showing semantic aspects of Unicode -- Isabelle/Scala merely (ab)uses the low-level rendering model (codepoint + font);
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
48416
5787e1c911d0 more ML_System operations;
wenzelm
parents: 43948
diff changeset
     4
ML system and platform operations.
43948
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
48416
5787e1c911d0 more ML_System operations;
wenzelm
parents: 43948
diff changeset
    14
  val share_common_data: unit -> unit
5787e1c911d0 more ML_System operations;
wenzelm
parents: 43948
diff changeset
    15
  val save_state: string -> unit
43948
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    16
end;
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    17
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    18
structure ML_System: ML_SYSTEM =
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    19
struct
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    20
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    21
val SOME name = OS.Process.getEnv "ML_SYSTEM";
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    22
val is_polyml = String.isPrefix "polyml" name;
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    23
val is_smlnj = String.isPrefix "smlnj" name;
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    24
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    25
val SOME platform = OS.Process.getEnv "ML_PLATFORM";
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    26
val platform_is_cygwin = String.isSuffix "cygwin" platform;
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    27
48416
5787e1c911d0 more ML_System operations;
wenzelm
parents: 43948
diff changeset
    28
fun share_common_data () = ();
5787e1c911d0 more ML_System operations;
wenzelm
parents: 43948
diff changeset
    29
fun save_state _ = raise Fail "Cannot save state -- undefined operation";
5787e1c911d0 more ML_System operations;
wenzelm
parents: 43948
diff changeset
    30
43948
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    31
end;
8f5add916a99 explicit structure ML_System;
wenzelm
parents:
diff changeset
    32