author | haftmann |
Mon, 08 Feb 2010 17:12:22 +0100 | |
changeset 35045 | a77d200e6503 |
parent 30671 | 2f64540707d6 |
child 56275 | 600f432ab556 |
permissions | -rw-r--r-- |
28267
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/ml_name_space.ML |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
3 |
|
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
4 |
ML name space -- dummy version of Poly/ML 5.2 facility. |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
5 |
*) |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
6 |
|
30671 | 7 |
structure ML_Name_Space = |
28267
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
8 |
struct |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
9 |
|
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
10 |
type valueVal = unit; |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
11 |
type typeVal = unit; |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
12 |
type fixityVal = unit; |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
13 |
type structureVal = unit; |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
14 |
type signatureVal = unit; |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
15 |
type functorVal = unit; |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
16 |
|
30671 | 17 |
type T = |
28267
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
18 |
{lookupVal: string -> valueVal option, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
19 |
lookupType: string -> typeVal option, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
20 |
lookupFix: string -> fixityVal option, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
21 |
lookupStruct: string -> structureVal option, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
22 |
lookupSig: string -> signatureVal option, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
23 |
lookupFunct: string -> functorVal option, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
24 |
enterVal: string * valueVal -> unit, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
25 |
enterType: string * typeVal -> unit, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
26 |
enterFix: string * fixityVal -> unit, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
27 |
enterStruct: string * structureVal -> unit, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
28 |
enterSig: string * signatureVal -> unit, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
29 |
enterFunct: string * functorVal -> unit, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
30 |
allVal: unit -> (string * valueVal) list, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
31 |
allType: unit -> (string * typeVal) list, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
32 |
allFix: unit -> (string * fixityVal) list, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
33 |
allStruct: unit -> (string * structureVal) list, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
34 |
allSig: unit -> (string * signatureVal) list, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
35 |
allFunct: unit -> (string * functorVal) list}; |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
36 |
|
30671 | 37 |
val global: T = |
28267
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
38 |
{lookupVal = fn _ => NONE, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
39 |
lookupType = fn _ => NONE, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
40 |
lookupFix = fn _ => NONE, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
41 |
lookupStruct = fn _ => NONE, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
42 |
lookupSig = fn _ => NONE, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
43 |
lookupFunct = fn _ => NONE, |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
44 |
enterVal = fn _ => (), |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
45 |
enterType = fn _ => (), |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
46 |
enterFix = fn _ => (), |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
47 |
enterStruct = fn _ => (), |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
48 |
enterSig = fn _ => (), |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
49 |
enterFunct = fn _ => (), |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
50 |
allVal = fn _ => [], |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
51 |
allType = fn _ => [], |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
52 |
allFix = fn _ => [], |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
53 |
allStruct = fn _ => [], |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
54 |
allSig = fn _ => [], |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
55 |
allFunct = fn _ => []}; |
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
56 |
|
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
57 |
end; |