src/Pure/RAW/ROOT_polyml.ML
changeset 62490 39d01eaf5292
parent 62472 01e2bd5b4027
child 62493 dd154240a53c
equal deleted inserted replaced
62489:36f11bc393a2 62490:39d01eaf5292
   162 
   162 
   163 use "RAW/ml_compiler_parameters.ML";
   163 use "RAW/ml_compiler_parameters.ML";
   164 if ML_System.name = "polyml-5.6"
   164 if ML_System.name = "polyml-5.6"
   165 then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else ();
   165 then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else ();
   166 
   166 
   167 use "RAW/use_context.ML";
       
   168 use "RAW/ml_positions.ML";
   167 use "RAW/ml_positions.ML";
   169 use "RAW/compiler_polyml.ML";
   168 use "RAW/compiler_polyml.ML";
   170 
   169 
   171 PolyML.Compiler.reportUnreferencedIds := true;
   170 PolyML.Compiler.reportUnreferencedIds := true;
   172 PolyML.Compiler.printInAlphabeticalOrder := false;
   171 PolyML.Compiler.printInAlphabeticalOrder := false;
   184 
   183 
   185 
   184 
   186 (* ML debugger *)
   185 (* ML debugger *)
   187 
   186 
   188 if ML_System.name = "polyml-5.6"
   187 if ML_System.name = "polyml-5.6"
   189 then use "RAW/ml_debugger_polyml-5.6.ML"
   188 then use_no_debug "RAW/ml_debugger_polyml-5.6.ML"
   190 else use "RAW/ml_debugger.ML";
   189 else use_no_debug "RAW/ml_debugger.ML";