src/Pure/ML-Systems/polyml-5.2.ML
author wenzelm
Sat Nov 27 16:29:53 2010 +0100 (2010-11-27 ago)
changeset 40748 591b6778d076
parent 39616 8052101883c3
permissions -rw-r--r--
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm@33538
     1
(*  Title:      Pure/ML-Systems/polyml-5.2.ML
wenzelm@2341
     2
wenzelm@33538
     3
Compatibility wrapper for Poly/ML 5.2.
wenzelm@2341
     4
*)
wenzelm@2341
     5
wenzelm@28152
     6
open Thread;
wenzelm@30672
     7
wenzelm@30672
     8
structure ML_Name_Space =
wenzelm@30672
     9
struct
wenzelm@30672
    10
  open PolyML.NameSpace;
wenzelm@30672
    11
  type T = PolyML.NameSpace.nameSpace;
wenzelm@30672
    12
  val global = PolyML.globalNameSpace;
wenzelm@30672
    13
end;
wenzelm@30672
    14
wenzelm@31427
    15
fun reraise exn = raise exn;
wenzelm@31427
    16
wenzelm@26215
    17
use "ML-Systems/polyml_common.ML";
wenzelm@33538
    18
use "ML-Systems/thread_dummy.ML";
wenzelm@33538
    19
use "ML-Systems/multithreading.ML";
wenzelm@39616
    20
use "ML-Systems/unsynchronized.ML";
wenzelm@39616
    21
wenzelm@39616
    22
val _ = PolyML.Compiler.forgetValue "ref";
wenzelm@39616
    23
val _ = PolyML.Compiler.forgetType "ref";
wenzelm@26215
    24
wenzelm@26215
    25
val pointer_eq = PolyML.pointerEq;
wenzelm@23921
    26
wenzelm@29638
    27
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
wenzelm@29638
    28
wenzelm@31312
    29
use "ML-Systems/compiler_polyml-5.2.ML";
wenzelm@31313
    30
use "ML-Systems/pp_polyml.ML";
wenzelm@38635
    31
use "ML-Systems/pp_dummy.ML";
wenzelm@30627
    32