|
(* Title: Pure/ML/ml_init.ML
Author: Makarius
Initial ML environment.
*)
val seconds = Time.fromReal;
val _ =
List.app ML_Name_Space.forget_val
["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"];
val ord = SML90.ord;
val chr = SML90.chr;
val raw_explode = SML90.explode;
val implode = String.concat;
val pointer_eq = PolyML.pointerEq;
val error_depth = PolyML.error_depth;
open Thread;
datatype illegal = Interrupt;
structure Basic_Exn: BASIC_EXN = Exn;
open Basic_Exn;
structure String =
struct
open String;
fun substring (s, i, n) =
if n = 1 then String.str (String.sub (s, i))
else String.substring (s, i, n);
end;
(* FIXME workaround for 100% CPU usage in OS.Process.sleep *)
structure OS =
struct
open OS;
structure Process =
struct
open Process;
fun sleep t =
let
open Thread;
val lock = Mutex.mutex ();
val cond = ConditionVar.conditionVar ();
in ConditionVar.waitUntil (cond, lock, Time.now () + t) end;
end;
end;
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
