| author | haftmann |
| Sat, 27 Nov 2010 19:42:41 +0100 | |
| changeset 40763 | c0bfead42774 |
| parent 39616 | 8052101883c3 |
| child 43948 | 8f5add916a99 |
| 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 |
open Thread; |
|
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 |
structure ML_Name_Space = |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
9 |
struct |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
10 |
open PolyML.NameSpace; |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
11 |
type T = PolyML.NameSpace.nameSpace; |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
12 |
val global = PolyML.globalNameSpace; |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
13 |
end; |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
14 |
|
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
15 |
fun reraise exn = raise exn; |
|
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 |
use "ML-Systems/polyml_common.ML"; |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
18 |
use "ML-Systems/multithreading_polyml.ML"; |
|
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38635
diff
changeset
|
19 |
use "ML-Systems/unsynchronized.ML"; |
|
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38635
diff
changeset
|
20 |
|
|
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38635
diff
changeset
|
21 |
val _ = PolyML.Compiler.forgetValue "ref"; |
|
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38635
diff
changeset
|
22 |
val _ = PolyML.Compiler.forgetType "ref"; |
|
33538
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 |
val pointer_eq = PolyML.pointerEq; |
|
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 |
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
|
27 |
|
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
28 |
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
|
29 |
use "ML-Systems/pp_polyml.ML"; |
|
38635
f76ad0771f67
added ML toplevel pretty-printing for tables, using dummy for anything other than Poly/ML 5.3.0 (or later);
wenzelm
parents:
33538
diff
changeset
|
30 |
use "ML-Systems/pp_dummy.ML"; |
|
33538
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
31 |