1(* Title: Pure/ML/ml_init.ML 2 Author: Makarius 3 4Initial ML environment. 5*) 6 7structure PolyML_Pretty = 8struct 9 datatype context = datatype PolyML.context; 10 datatype pretty = datatype PolyML.pretty; 11end; 12 13val seconds = Time.fromReal; 14 15val _ = 16 List.app ML_Name_Space.forget_val 17 ["isSome", "getOpt", "valOf", "foldl", "foldr", "print", "explode", "concat"]; 18 19val ord = SML90.ord; 20val chr = SML90.chr; 21val raw_explode = SML90.explode; 22val implode = String.concat; 23 24val pointer_eq = PolyML.pointerEq; 25 26val error_depth = PolyML.error_depth; 27 28open Thread; 29 30datatype illegal = Interrupt; 31 32structure Basic_Exn: BASIC_EXN = Exn; 33open Basic_Exn; 34 35structure String = 36struct 37 open String; 38 fun substring (s, i, n) = 39 if n = 1 then String.str (String.sub (s, i)) 40 else String.substring (s, i, n); 41end; 42