1 (* Title: Pure/RAW/ml_name_space.ML |
|
2 Author: Makarius |
|
3 |
|
4 Name space for Poly/ML. |
|
5 *) |
|
6 |
|
7 structure ML_Name_Space = |
|
8 struct |
|
9 open PolyML.NameSpace; |
|
10 |
|
11 type T = PolyML.NameSpace.nameSpace; |
|
12 val global = PolyML.globalNameSpace; |
|
13 val forget_global_structure = PolyML.Compiler.forgetStructure; |
|
14 |
|
15 type valueVal = Values.value; |
|
16 fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space); |
|
17 fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space); |
|
18 val initial_val = |
|
19 List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit") |
|
20 (#allVal global ()); |
|
21 |
|
22 type typeVal = TypeConstrs.typeConstr; |
|
23 fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space); |
|
24 val initial_type = #allType global (); |
|
25 |
|
26 type fixityVal = Infixes.fixity; |
|
27 fun displayFix (_: string, x) = Infixes.print x; |
|
28 val initial_fixity = #allFix global (); |
|
29 |
|
30 type structureVal = Structures.structureVal; |
|
31 fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space); |
|
32 val initial_structure = #allStruct global (); |
|
33 |
|
34 type signatureVal = Signatures.signatureVal; |
|
35 fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space); |
|
36 val initial_signature = #allSig global (); |
|
37 |
|
38 type functorVal = Functors.functorVal; |
|
39 fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space); |
|
40 val initial_functor = #allFunct global (); |
|
41 end; |
|