author | wenzelm |
Thu, 03 Mar 2016 22:24:58 +0100 | |
changeset 62510 | 77a5f21c449b |
parent 62508 | d0b68218ea55 |
child 62657 | cdd6db02eae8 |
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 |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
9 |
open PolyML.NameSpace; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
10 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
11 |
type T = PolyML.NameSpace.nameSpace; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
12 |
val global = PolyML.globalNameSpace; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
13 |
val forget_global_structure = PolyML.Compiler.forgetStructure; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
14 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
15 |
type valueVal = Values.value; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
16 |
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
|
17 |
fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space); |
62510 | 18 |
val initial_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ()); |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
19 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
20 |
type typeVal = TypeConstrs.typeConstr; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
21 |
fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space); |
62504 | 22 |
val initial_type = #allType global (); |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
23 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
24 |
type fixityVal = Infixes.fixity; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
25 |
fun displayFix (_: string, x) = Infixes.print x; |
62504 | 26 |
val initial_fixity = #allFix global (); |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
27 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
28 |
type structureVal = Structures.structureVal; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
29 |
fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space); |
62504 | 30 |
val initial_structure = #allStruct global (); |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
31 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
32 |
type signatureVal = Signatures.signatureVal; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
33 |
fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space); |
62504 | 34 |
val initial_signature = #allSig global (); |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
35 |
|
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
36 |
type functorVal = Functors.functorVal; |
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
37 |
fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space); |
62504 | 38 |
val initial_functor = #allFunct global (); |
61715
5dc95d957569
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff
changeset
|
39 |
end; |