src/Pure/ML/ml_name_space.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62934 6e3fb0aa857a
child 68815 6296915dee6e
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      Pure/ML/ml_name_space.ML
     2     Author:     Makarius
     3 
     4 ML name space, with initial entries for strict Standard ML.
     5 *)
     6 
     7 signature ML_NAME_SPACE =
     8 sig
     9   type T
    10   val global: T
    11   val global_values: (string * string) list -> T
    12   val forget_val: string -> unit
    13   val forget_type: string -> unit
    14   val forget_structure: string -> unit
    15   val bootstrap_values: string list
    16   val hidden_structures: string list
    17   val bootstrap_structures: string list
    18   val bootstrap_signatures: string list
    19   val sml_val: (string * PolyML.NameSpace.Values.value) list
    20   val sml_type: (string * PolyML.NameSpace.TypeConstrs.typeConstr) list
    21   val sml_fixity: (string * PolyML.NameSpace.Infixes.fixity) list
    22   val sml_structure: (string * PolyML.NameSpace.Structures.structureVal) list
    23   val sml_signature: (string * PolyML.NameSpace.Signatures.signatureVal) list
    24   val sml_functor: (string * PolyML.NameSpace.Functors.functorVal) list
    25 end;
    26 
    27 structure ML_Name_Space: ML_NAME_SPACE =
    28 struct
    29 
    30 type T = PolyML.NameSpace.nameSpace;
    31 
    32 
    33 (* global *)
    34 
    35 val global = PolyML.globalNameSpace;
    36 fun global_values values : T =
    37  {lookupVal = #lookupVal global,
    38   lookupType = #lookupType global,
    39   lookupStruct = #lookupStruct global,
    40   lookupFix = #lookupFix global,
    41   lookupSig = #lookupSig global,
    42   lookupFunct = #lookupFunct global,
    43   enterVal =
    44     fn (x, value) =>
    45       (case List.find (fn (y, _) => x = y) values of
    46         SOME (_, x') => #enterVal global (x', value)
    47       | NONE => ()),
    48   enterType = fn _ => (),
    49   enterFix = fn _ => (),
    50   enterStruct = fn _ => (),
    51   enterSig = fn _ => (),
    52   enterFunct = fn _ => (),
    53   allVal = #allVal global,
    54   allType = #allType global,
    55   allFix = #allFix global,
    56   allStruct = #allStruct global,
    57   allSig = #allSig global,
    58   allFunct = #allFunct global};
    59 
    60 
    61 (* forget entries *)
    62 
    63 val forget_val = PolyML.Compiler.forgetValue;
    64 val forget_type = PolyML.Compiler.forgetType;
    65 val forget_structure = PolyML.Compiler.forgetStructure;
    66 
    67 
    68 (* bootstrap environment *)
    69 
    70 val bootstrap_values =
    71   ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload",
    72     "chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
    73 val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
    74 val bootstrap_structures =
    75   ["Exn", "Output_Primitives", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive",
    76     "Private_Output", "PolyML"] @ hidden_structures;
    77 val bootstrap_signatures =
    78   ["EXN", "OUTPUT_PRIMITIVES", "BASIC_EXN", "THREAD_DATA", "THREAD_POSITION", "ML_RECURSIVE",
    79     "PRIVATE_OUTPUT", "ML_NAME_SPACE"];
    80 
    81 
    82 (* Standard ML environment *)
    83 
    84 val sml_val =
    85   List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_values) (#allVal global ());
    86 val sml_type = #allType global ();
    87 val sml_fixity = #allFix global ();
    88 val sml_structure =
    89   List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_structures) (#allStruct global ());
    90 val sml_signature =
    91   List.filter (fn (a, _) => List.all (fn b => a <> b) bootstrap_signatures) (#allSig global ());
    92 val sml_functor = #allFunct global ();
    93 
    94 end;