src/Pure/ML-Systems/polyml.ML
changeset 56275 600f432ab556
parent 54723 124432e77ecf
child 56281 03c3d1a7c3b8
     1.1 --- a/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 10:37:10 2014 +0100
     1.2 +++ b/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 13:18:10 2014 +0100
     1.3 @@ -4,6 +4,24 @@
     1.4  Compatibility wrapper for Poly/ML.
     1.5  *)
     1.6  
     1.7 +(* ML name space *)
     1.8 +
     1.9 +structure ML_Name_Space =
    1.10 +struct
    1.11 +  open PolyML.NameSpace;
    1.12 +  type T = PolyML.NameSpace.nameSpace;
    1.13 +  val global = PolyML.globalNameSpace;
    1.14 +  val initial_val =
    1.15 +    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
    1.16 +      (#allVal global ());
    1.17 +  val initial_type = #allType global ();
    1.18 +  val initial_fixity = #allFix global ();
    1.19 +  val initial_structure = #allStruct global ();
    1.20 +  val initial_signature = #allSig global ();
    1.21 +  val initial_functor = #allFunct global ();
    1.22 +end;
    1.23 +
    1.24 +
    1.25  (* ML system operations *)
    1.26  
    1.27  use "ML-Systems/ml_system.ML";
    1.28 @@ -94,13 +112,6 @@
    1.29  
    1.30  (* ML compiler *)
    1.31  
    1.32 -structure ML_Name_Space =
    1.33 -struct
    1.34 -  open PolyML.NameSpace;
    1.35 -  type T = PolyML.NameSpace.nameSpace;
    1.36 -  val global = PolyML.globalNameSpace;
    1.37 -end;
    1.38 -
    1.39  use "ML-Systems/use_context.ML";
    1.40  use "ML-Systems/compiler_polyml.ML";
    1.41