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