src/Pure/ML/ml_compiler_polyml-5.3.ML
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-02 wenzelm 2009-09-02 updated Poly/ML SVN version;
2009-09-02 wenzelm 2009-09-02 eval/location_props: always produce YXML markup, independent of print_mode;
2009-09-02 wenzelm 2009-09-02 tuned ML message;
2009-06-22 wenzelm 2009-06-22 eval: tuned input buffer and get_offset (which ran very hot, up to the point where AFP/FlyspeckTame would seemingly take forever);
2009-06-06 wenzelm 2009-06-06 updated version;
2009-06-06 wenzelm 2009-06-06 reraise exceptions to preserve position information;
2009-06-06 wenzelm 2009-06-06 added exn_message (formerly in toplevel.ML); eval/code: proper Isar runtime support; tuned signature;
2009-06-06 wenzelm 2009-06-06 report_parse_tree: ML_open, ML_struct; eval: terminate input by explicit end token, to ensure that Poly/ML attaches proper position to last input token; tuned;
2009-06-04 wenzelm 2009-06-04 removed unused location_of; eval: actually pass location properties (via "file" field);
2009-06-04 wenzelm 2009-06-04 more robust treatment of bootstrap source positions;
2009-06-04 wenzelm 2009-06-04 convert explicitly between Position.T/PolyML.location, without costly registration of tokens; added exception_position;
2009-06-01 wenzelm 2009-06-01 added structure ML_Compiler: runtime compilation, with advanced version for Poly/ML 5.3 (formerly ML_Test);