author | wenzelm |
Wed, 17 Aug 2011 23:37:23 +0200 | |
changeset 44249 | 64620f1d6f87 |
parent 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; |
44249
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
16 |
fun set_exn_serial (_: int) (exn: exn) = exn; |
64620f1d6f87
identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
wenzelm
parents:
43948
diff
changeset
|
17 |
fun get_exn_serial (exn: exn) : int option = NONE; |
33538
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"; |
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38635
diff
changeset
|
21 |
use "ML-Systems/unsynchronized.ML"; |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38635
diff
changeset
|
22 |
|
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38635
diff
changeset
|
23 |
val _ = PolyML.Compiler.forgetValue "ref"; |
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
38635
diff
changeset
|
24 |
val _ = PolyML.Compiler.forgetType "ref"; |
33538
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 |
val pointer_eq = PolyML.pointerEq; |
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 |
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
|
29 |
|
edf497b5b5d2
setup for official Poly/ML 5.3.0, which is now the default;
wenzelm
parents:
diff
changeset
|
30 |
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
|
31 |
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
|
32 |
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
|
33 |
|
43948 | 34 |
use "ML-Systems/ml_system.ML"; |
35 |