src/Pure/ML-Systems/polyml-5.2.1.ML
author wenzelm
Sat Nov 27 16:29:53 2010 +0100 (2010-11-27 ago)
changeset 40748 591b6778d076
parent 39616 8052101883c3
child 43948 8f5add916a99
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.1.ML
wenzelm@33538
     2
wenzelm@33538
     3
Compatibility wrapper for Poly/ML 5.2.1.
wenzelm@33538
     4
*)
wenzelm@33538
     5
wenzelm@33538
     6
open Thread;
wenzelm@33538
     7
wenzelm@33538
     8
structure ML_Name_Space =
wenzelm@33538
     9
struct
wenzelm@33538
    10
  open PolyML.NameSpace;
wenzelm@33538
    11
  type T = PolyML.NameSpace.nameSpace;
wenzelm@33538
    12
  val global = PolyML.globalNameSpace;
wenzelm@33538
    13
end;
wenzelm@33538
    14
wenzelm@33538
    15
fun reraise exn = raise exn;
wenzelm@33538
    16
wenzelm@33538
    17
use "ML-Systems/polyml_common.ML";
wenzelm@33538
    18
use "ML-Systems/multithreading_polyml.ML";
wenzelm@39616
    19
use "ML-Systems/unsynchronized.ML";
wenzelm@39616
    20
wenzelm@39616
    21
val _ = PolyML.Compiler.forgetValue "ref";
wenzelm@39616
    22
val _ = PolyML.Compiler.forgetType "ref";
wenzelm@33538
    23
wenzelm@33538
    24
val pointer_eq = PolyML.pointerEq;
wenzelm@33538
    25
wenzelm@33538
    26
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
wenzelm@33538
    27
wenzelm@33538
    28
use "ML-Systems/compiler_polyml-5.2.ML";
wenzelm@33538
    29
use "ML-Systems/pp_polyml.ML";
wenzelm@38635
    30
use "ML-Systems/pp_dummy.ML";
wenzelm@33538
    31