author | huffman |
Sun, 07 Mar 2010 13:34:53 -0800 | |
changeset 35640 | 9617aeca7147 |
parent 33538 | edf497b5b5d2 |
child 38635 | f76ad0771f67 |
permissions | -rw-r--r-- |
33538
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/polyml-5.2.1.ML |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
2 |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
3 |
Compatibility wrapper for Poly/ML 5.2.1. |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
4 |
*) |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
5 |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
6 |
use "ML-Systems/unsynchronized.ML"; |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
7 |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
8 |
open Thread; |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
9 |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
10 |
structure ML_Name_Space = |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
11 |
struct |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
12 |
open PolyML.NameSpace; |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
13 |
type T = PolyML.NameSpace.nameSpace; |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
14 |
val global = PolyML.globalNameSpace; |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
15 |
end; |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
16 |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
17 |
fun reraise exn = raise exn; |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
18 |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
19 |
use "ML-Systems/polyml_common.ML"; |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
20 |
use "ML-Systems/multithreading_polyml.ML"; |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
21 |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
22 |
val pointer_eq = PolyML.pointerEq; |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
23 |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
24 |
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
25 |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
26 |
use "ML-Systems/compiler_polyml-5.2.ML"; |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
27 |
use "ML-Systems/pp_polyml.ML"; |
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
28 |