1 (* Title: Pure/RAW/ml_name_space.ML |
|
2 Author: Makarius |
|
3 |
|
4 ML name space -- dummy version of Poly/ML 5.2 facility. |
|
5 *) |
|
6 |
|
7 structure ML_Name_Space = |
|
8 struct |
|
9 |
|
10 type valueVal = unit; |
|
11 type typeVal = unit; |
|
12 type fixityVal = unit; |
|
13 type structureVal = unit; |
|
14 type signatureVal = unit; |
|
15 type functorVal = unit; |
|
16 |
|
17 type T = |
|
18 {lookupVal: string -> valueVal option, |
|
19 lookupType: string -> typeVal option, |
|
20 lookupFix: string -> fixityVal option, |
|
21 lookupStruct: string -> structureVal option, |
|
22 lookupSig: string -> signatureVal option, |
|
23 lookupFunct: string -> functorVal option, |
|
24 enterVal: string * valueVal -> unit, |
|
25 enterType: string * typeVal -> unit, |
|
26 enterFix: string * fixityVal -> unit, |
|
27 enterStruct: string * structureVal -> unit, |
|
28 enterSig: string * signatureVal -> unit, |
|
29 enterFunct: string * functorVal -> unit, |
|
30 allVal: unit -> (string * valueVal) list, |
|
31 allType: unit -> (string * typeVal) list, |
|
32 allFix: unit -> (string * fixityVal) list, |
|
33 allStruct: unit -> (string * structureVal) list, |
|
34 allSig: unit -> (string * signatureVal) list, |
|
35 allFunct: unit -> (string * functorVal) list}; |
|
36 |
|
37 val global: T = |
|
38 {lookupVal = fn _ => NONE, |
|
39 lookupType = fn _ => NONE, |
|
40 lookupFix = fn _ => NONE, |
|
41 lookupStruct = fn _ => NONE, |
|
42 lookupSig = fn _ => NONE, |
|
43 lookupFunct = fn _ => NONE, |
|
44 enterVal = fn _ => (), |
|
45 enterType = fn _ => (), |
|
46 enterFix = fn _ => (), |
|
47 enterStruct = fn _ => (), |
|
48 enterSig = fn _ => (), |
|
49 enterFunct = fn _ => (), |
|
50 allVal = fn _ => [], |
|
51 allType = fn _ => [], |
|
52 allFix = fn _ => [], |
|
53 allStruct = fn _ => [], |
|
54 allSig = fn _ => [], |
|
55 allFunct = fn _ => []}; |
|
56 |
|
57 val initial_val : (string * valueVal) list = []; |
|
58 val initial_type : (string * typeVal) list = []; |
|
59 val initial_fixity : (string * fixityVal) list = []; |
|
60 val initial_structure : (string * structureVal) list = []; |
|
61 val initial_signature : (string * signatureVal) list = []; |
|
62 val initial_functor : (string * functorVal) list = []; |
|
63 |
|
64 fun forget_global_structure (_: string) = (); |
|
65 |
|
66 fun display_val (_, _: int, _: T) = ML_Pretty.String ("?", 1); |
|
67 |
|
68 end; |
|