src/Pure/ML-Systems/ml_name_space.ML
author wenzelm
Sun, 31 May 2009 14:51:21 +0200
changeset 31312 1c00e4ff3c99
parent 30671 2f64540707d6
child 56275 600f432ab556
permissions -rw-r--r--
more modular setup of runtime compilation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
2f64540707d6 de-camelized ML_Name_Space;
wenzelm
parents: 29564
diff changeset
     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
2f64540707d6 de-camelized ML_Name_Space;
wenzelm
parents: 29564
diff changeset
    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
2f64540707d6 de-camelized ML_Name_Space;
wenzelm
parents: 29564
diff changeset
    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;