author | wenzelm |
Sat Nov 27 16:29:53 2010 +0100 (2010-11-27 ago) | |
changeset 40748 | 591b6778d076 |
parent 39616 | 8052101883c3 |
permissions | -rw-r--r-- |
wenzelm@33538 | 1 |
(* Title: Pure/ML-Systems/polyml-5.2.ML |
wenzelm@2341 | 2 |
|
wenzelm@33538 | 3 |
Compatibility wrapper for Poly/ML 5.2. |
wenzelm@2341 | 4 |
*) |
wenzelm@2341 | 5 |
|
wenzelm@28152 | 6 |
open Thread; |
wenzelm@30672 | 7 |
|
wenzelm@30672 | 8 |
structure ML_Name_Space = |
wenzelm@30672 | 9 |
struct |
wenzelm@30672 | 10 |
open PolyML.NameSpace; |
wenzelm@30672 | 11 |
type T = PolyML.NameSpace.nameSpace; |
wenzelm@30672 | 12 |
val global = PolyML.globalNameSpace; |
wenzelm@30672 | 13 |
end; |
wenzelm@30672 | 14 |
|
wenzelm@31427 | 15 |
fun reraise exn = raise exn; |
wenzelm@31427 | 16 |
|
wenzelm@26215 | 17 |
use "ML-Systems/polyml_common.ML"; |
wenzelm@33538 | 18 |
use "ML-Systems/thread_dummy.ML"; |
wenzelm@33538 | 19 |
use "ML-Systems/multithreading.ML"; |
wenzelm@39616 | 20 |
use "ML-Systems/unsynchronized.ML"; |
wenzelm@39616 | 21 |
|
wenzelm@39616 | 22 |
val _ = PolyML.Compiler.forgetValue "ref"; |
wenzelm@39616 | 23 |
val _ = PolyML.Compiler.forgetType "ref"; |
wenzelm@26215 | 24 |
|
wenzelm@26215 | 25 |
val pointer_eq = PolyML.pointerEq; |
wenzelm@23921 | 26 |
|
wenzelm@29638 | 27 |
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
wenzelm@29638 | 28 |
|
wenzelm@31312 | 29 |
use "ML-Systems/compiler_polyml-5.2.ML"; |
wenzelm@31313 | 30 |
use "ML-Systems/pp_polyml.ML"; |
wenzelm@38635 | 31 |
use "ML-Systems/pp_dummy.ML"; |
wenzelm@30627 | 32 |