equal
deleted
inserted
replaced
1 (* Title: Pure/ML/ml_name_space.ML |
1 (* Title: Pure/ML/ml_name_space.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Name space for Poly/ML. |
4 ML name space, with initial entries for strict Standard ML. |
5 *) |
5 *) |
6 |
6 |
7 structure ML_Name_Space = |
7 structure ML_Name_Space = |
8 struct |
8 struct |
9 val critical_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"]; |
|
10 |
|
11 open PolyML.NameSpace; |
9 open PolyML.NameSpace; |
12 |
10 |
13 type T = PolyML.NameSpace.nameSpace; |
11 type T = PolyML.NameSpace.nameSpace; |
14 |
12 |
15 val global = PolyML.globalNameSpace; |
13 val global = PolyML.globalNameSpace; |
65 val sml_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ()); |
63 val sml_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ()); |
66 val sml_type = #allType global (); |
64 val sml_type = #allType global (); |
67 val sml_fixity = #allFix global (); |
65 val sml_fixity = #allFix global (); |
68 val sml_structure = |
66 val sml_structure = |
69 List.filter (fn (a, _) => |
67 List.filter (fn (a, _) => |
70 not (List.exists (fn b => a = b) |
68 List.all (fn b => a <> b) |
71 ["ML_System", "PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"])) |
69 ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"]) |
72 (#allStruct global ()); |
70 (#allStruct global ()); |
73 val sml_signature = |
71 val sml_signature = #allSig global (); |
74 List.filter (fn (a, _) => a <> "ML_SYSTEM" andalso a <> "ML_NAME_SPACE") (#allSig global ()); |
|
75 val sml_functor = #allFunct global (); |
72 val sml_functor = #allFunct global (); |
76 end; |
73 end; |