author | wenzelm |
Thu, 17 Mar 2016 10:54:28 +0100 | |
changeset 62659 | bb29cc00c31f |
parent 62657 | cdd6db02eae8 |
child 62819 | d3ff367a16a0 |
permissions | -rw-r--r-- |
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62504
diff
changeset
|
1 |
(* Title: Pure/ML/ml_name_space.ML |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
3 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
4 |
Name space for Poly/ML. |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
5 |
*) |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
6 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
7 |
structure ML_Name_Space = |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
8 |
struct |
62659
bb29cc00c31f
hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
wenzelm
parents:
62657
diff
changeset
|
9 |
val critical_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"]; |
bb29cc00c31f
hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
wenzelm
parents:
62657
diff
changeset
|
10 |
|
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
11 |
open PolyML.NameSpace; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
12 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
13 |
type T = PolyML.NameSpace.nameSpace; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
14 |
val global = PolyML.globalNameSpace; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
15 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
16 |
type valueVal = Values.value; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
17 |
fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space); |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
18 |
fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space); |
62510 | 19 |
val initial_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ()); |
62657 | 20 |
val forget_val = PolyML.Compiler.forgetValue; |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
21 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
22 |
type typeVal = TypeConstrs.typeConstr; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
23 |
fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space); |
62504 | 24 |
val initial_type = #allType global (); |
62657 | 25 |
val forget_type = PolyML.Compiler.forgetType; |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
26 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
27 |
type fixityVal = Infixes.fixity; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
28 |
fun displayFix (_: string, x) = Infixes.print x; |
62504 | 29 |
val initial_fixity = #allFix global (); |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
30 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
31 |
type structureVal = Structures.structureVal; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
32 |
fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space); |
62659
bb29cc00c31f
hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
wenzelm
parents:
62657
diff
changeset
|
33 |
val initial_structure = |
bb29cc00c31f
hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
wenzelm
parents:
62657
diff
changeset
|
34 |
List.filter (fn (a, _) => not (List.exists (fn b => a = b) critical_structures)) |
bb29cc00c31f
hide critical structures of Poly/ML, to make it harder to disrupt the ML environment;
wenzelm
parents:
62657
diff
changeset
|
35 |
(#allStruct global ()); |
62657 | 36 |
val forget_structure = PolyML.Compiler.forgetStructure; |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
37 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
38 |
type signatureVal = Signatures.signatureVal; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
39 |
fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space); |
62504 | 40 |
val initial_signature = #allSig global (); |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
41 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
42 |
type functorVal = Functors.functorVal; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
43 |
fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space); |
62504 | 44 |
val initial_functor = #allFunct global (); |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
45 |
end; |