| author | wenzelm |
| Sat, 27 Feb 2010 13:32:38 +0100 | |
| changeset 35396 | 041bb8d18916 |
| 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 |