src/Pure/ML/ml_name_space.ML
changeset 62839 ea9f12e422c7
parent 62819 d3ff367a16a0
child 62851 07eea2843b82
equal deleted inserted replaced
62838:c91ca9935280 62839:ea9f12e422c7
    38     allFunct = #allFunct global};
    38     allFunct = #allFunct global};
    39 
    39 
    40   type valueVal = Values.value;
    40   type valueVal = Values.value;
    41   fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
    41   fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
    42   fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
    42   fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
    43   val initial_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
       
    44   val forget_val = PolyML.Compiler.forgetValue;
    43   val forget_val = PolyML.Compiler.forgetValue;
    45 
    44 
    46   type typeVal = TypeConstrs.typeConstr;
    45   type typeVal = TypeConstrs.typeConstr;
    47   fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
    46   fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
    48   val initial_type = #allType global ();
       
    49   val forget_type = PolyML.Compiler.forgetType;
    47   val forget_type = PolyML.Compiler.forgetType;
    50 
    48 
    51   type fixityVal = Infixes.fixity;
    49   type fixityVal = Infixes.fixity;
    52   fun displayFix (_: string, x) = Infixes.print x;
    50   fun displayFix (_: string, x) = Infixes.print x;
    53   val initial_fixity = #allFix global ();
       
    54 
    51 
    55   type structureVal = Structures.structureVal;
    52   type structureVal = Structures.structureVal;
    56   fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
    53   fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
    57   val initial_structure =
       
    58     List.filter (fn (a, _) => not (List.exists (fn b => a = b) critical_structures))
       
    59       (#allStruct global ());
       
    60   val forget_structure = PolyML.Compiler.forgetStructure;
    54   val forget_structure = PolyML.Compiler.forgetStructure;
    61 
    55 
    62   type signatureVal = Signatures.signatureVal;
    56   type signatureVal = Signatures.signatureVal;
    63   fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
    57   fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
    64   val initial_signature = #allSig global ();
       
    65 
    58 
    66   type functorVal = Functors.functorVal;
    59   type functorVal = Functors.functorVal;
    67   fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
    60   fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
    68   val initial_functor = #allFunct global ();
    61 
       
    62 
       
    63   (* Standard ML name space *)
       
    64 
       
    65   val sml_val = List.filter (fn (a, _) => a <> "use" andalso a <> "exit") (#allVal global ());
       
    66   val sml_type = #allType global ();
       
    67   val sml_fixity = #allFix global ();
       
    68   val sml_structure =
       
    69     List.filter (fn (a, _) => a <> "PolyML" andalso a <> "ML_System" andalso
       
    70       not (List.exists (fn b => a = b) critical_structures)) (#allStruct global ());
       
    71   val sml_signature =
       
    72     List.filter (fn (a, _) => a <> "ML_SYSTEM" andalso a <> "ML_NAME_SPACE") (#allSig global ());
       
    73   val sml_functor = #allFunct global ();
    69 end;
    74 end;