author | wenzelm |
Tue, 11 Aug 2015 20:05:27 +0200 | |
changeset 60897 | 7aad4be8a48e |
parent 59127 | 723b11f8ffbf |
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 |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
30671
diff
changeset
|
57 |
val initial_val : (string * valueVal) list = []; |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
30671
diff
changeset
|
58 |
val initial_type : (string * typeVal) list = []; |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
30671
diff
changeset
|
59 |
val initial_fixity : (string * fixityVal) list = []; |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
30671
diff
changeset
|
60 |
val initial_structure : (string * structureVal) list = []; |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
30671
diff
changeset
|
61 |
val initial_signature : (string * signatureVal) list = []; |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
30671
diff
changeset
|
62 |
val initial_functor : (string * functorVal) list = []; |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
30671
diff
changeset
|
63 |
|
59127
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
56275
diff
changeset
|
64 |
fun forget_global_structure (_: string) = (); |
723b11f8ffbf
more careful handling of auxiliary environment structure -- allow nested ML evaluation;
wenzelm
parents:
56275
diff
changeset
|
65 |
|
60897 | 66 |
fun display_val (_, _: int, _: T) = ML_Pretty.String ("?", 1); |
67 |
||
28267
596b0fd784a3
ML name space -- dummy version of Poly/ML 5.2 facility.
wenzelm
parents:
diff
changeset
|
68 |
end; |