equal
deleted
inserted
replaced
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Final setup of ML environment. |
4 Final setup of ML environment. |
5 *) |
5 *) |
6 |
6 |
7 (*no access to system internals!*) |
7 if Options.default_bool "ML_system_unsafe" then () |
8 structure PolyML = struct structure IntInf = PolyML.IntInf end; |
8 else |
9 val _ = List.app ML_Name_Space.forget_structure ML_Name_Space.critical_structures; |
9 (List.app ML_Name_Space.forget_structure |
|
10 ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"]; |
|
11 ML \<open>structure PolyML = struct structure IntInf = PolyML.IntInf end\<close>); |
10 |
12 |
11 structure Output: OUTPUT = Output; (*seal system channels!*) |
13 structure Output: OUTPUT = Output; (*seal system channels!*) |
12 |
14 |
13 structure Pure = struct val thy = Thy_Info.pure_theory () end; |
15 structure Pure = struct val thy = Thy_Info.pure_theory () end; |
14 |
16 |