src/Pure/ML/ml_name_space.ML
author wenzelm
Mon, 04 Apr 2016 20:28:17 +0200
changeset 62853 8e54fd480809
parent 62851 07eea2843b82
child 62860 045dc4ad6d98
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
62853
wenzelm
parents: 62851
diff changeset
     4
ML name space, with initial entries for strict Standard ML.
61715
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;
62819
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    12
61715
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    13
  val global = PolyML.globalNameSpace;
62819
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    14
  fun global_values values : T =
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    15
   {lookupVal = #lookupVal global,
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    16
    lookupType = #lookupType global,
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    17
    lookupStruct = #lookupStruct global,
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    18
    lookupFix = #lookupFix global,
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    19
    lookupSig = #lookupSig global,
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    20
    lookupFunct = #lookupFunct global,
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    21
    enterVal =
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    22
      fn (x, value) =>
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    23
        (case List.find (fn (y, _) => x = y) values of
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    24
          SOME (_, x') => #enterVal global (x', value)
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    25
        | NONE => ()),
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    26
    enterType = fn _ => (),
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    27
    enterFix = fn _ => (),
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    28
    enterStruct = fn _ => (),
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    29
    enterSig = fn _ => (),
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    30
    enterFunct = fn _ => (),
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    31
    allVal = #allVal global,
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    32
    allType = #allType global,
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    33
    allFix = #allFix global,
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    34
    allStruct = #allStruct global,
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    35
    allSig = #allSig global,
d3ff367a16a0 careful export of type-dependent functions, without losing their special status;
wenzelm
parents: 62659
diff changeset
    36
    allFunct = #allFunct global};
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 valueVal = Values.value;
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    39
  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
    40
  fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
62657
cdd6db02eae8 tuned signature;
wenzelm
parents: 62510
diff changeset
    41
  val forget_val = PolyML.Compiler.forgetValue;
61715
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    42
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    43
  type typeVal = TypeConstrs.typeConstr;
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    44
  fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
62657
cdd6db02eae8 tuned signature;
wenzelm
parents: 62510
diff changeset
    45
  val forget_type = PolyML.Compiler.forgetType;
61715
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    46
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    47
  type fixityVal = Infixes.fixity;
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    48
  fun displayFix (_: string, x) = Infixes.print x;
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    49
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    50
  type structureVal = Structures.structureVal;
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    51
  fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
62657
cdd6db02eae8 tuned signature;
wenzelm
parents: 62510
diff changeset
    52
  val forget_structure = PolyML.Compiler.forgetStructure;
61715
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    53
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    54
  type signatureVal = Signatures.signatureVal;
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    55
  fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    56
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    57
  type functorVal = Functors.functorVal;
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    58
  fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
62839
ea9f12e422c7 clarified SML name space: no access to structure PolyML;
wenzelm
parents: 62819
diff changeset
    59
ea9f12e422c7 clarified SML name space: no access to structure PolyML;
wenzelm
parents: 62819
diff changeset
    60
ea9f12e422c7 clarified SML name space: no access to structure PolyML;
wenzelm
parents: 62819
diff changeset
    61
  (* Standard ML name space *)
ea9f12e422c7 clarified SML name space: no access to structure PolyML;
wenzelm
parents: 62819
diff changeset
    62
ea9f12e422c7 clarified SML name space: no access to structure PolyML;
wenzelm
parents: 62819
diff changeset
    63
  val sml_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
ea9f12e422c7 clarified SML name space: no access to structure PolyML;
wenzelm
parents: 62819
diff changeset
    64
  val sml_type = #allType global ();
ea9f12e422c7 clarified SML name space: no access to structure PolyML;
wenzelm
parents: 62819
diff changeset
    65
  val sml_fixity = #allFix global ();
ea9f12e422c7 clarified SML name space: no access to structure PolyML;
wenzelm
parents: 62819
diff changeset
    66
  val sml_structure =
62851
07eea2843b82 option ML_system_unsafe;
wenzelm
parents: 62839
diff changeset
    67
    List.filter (fn (a, _) =>
62853
wenzelm
parents: 62851
diff changeset
    68
      List.all (fn b => a <> b)
wenzelm
parents: 62851
diff changeset
    69
        ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"])
62851
07eea2843b82 option ML_system_unsafe;
wenzelm
parents: 62839
diff changeset
    70
      (#allStruct global ());
62853
wenzelm
parents: 62851
diff changeset
    71
  val sml_signature = #allSig global ();
62839
ea9f12e422c7 clarified SML name space: no access to structure PolyML;
wenzelm
parents: 62819
diff changeset
    72
  val sml_functor = #allFunct global ();
61715
5dc95d957569 speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;
wenzelm
parents:
diff changeset
    73
end;