2009-06-04 wenzelm [Thu, 04 Jun 2009 19:15:54 +0200] rev 31433
less experimental polyml-5.3;
src/Pure/IsaMakefile src/Pure/ML-Systems/compiler_polyml-5.3.ML src/Pure/ML-Systems/install_pp_polyml-5.3.ML src/Pure/ML-Systems/install_pp_polyml-experimental.ML src/Pure/ML-Systems/polyml-experimental.ML src/Pure/pure_setup.ML

2009-06-04 wenzelm [Thu, 04 Jun 2009 18:00:47 +0200] rev 31432
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
src/Pure/Concurrent/ROOT.ML src/Pure/General/ROOT.ML src/Pure/IsaMakefile src/Pure/Isar/ROOT.ML src/Pure/ProofGeneral/ROOT.ML src/Pure/ROOT.ML src/Pure/Tools/ROOT.ML

2009-06-04 wenzelm [Thu, 04 Jun 2009 17:31:39 +0200] rev 31431
exn_message/raised: ML_Compiler.exception_position;
src/Pure/Isar/toplevel.ML

2009-06-04 wenzelm [Thu, 04 Jun 2009 17:31:39 +0200] rev 31430
eliminated costly registration of tokens;
src/Pure/ML/ml_env.ML

2009-06-04 wenzelm [Thu, 04 Jun 2009 17:31:38 +0200] rev 31429
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
added exception_position;
src/Pure/ML/ml_compiler_polyml-5.3.ML

2009-06-04 wenzelm [Thu, 04 Jun 2009 17:31:38 +0200] rev 31428
added exception_position (dummy);
src/Pure/ML/ml_compiler.ML

2009-06-04 wenzelm [Thu, 04 Jun 2009 17:31:38 +0200] rev 31427
reraise exceptions to preserve original position (ML system specific);
src/Pure/ML-Systems/exn.ML src/Pure/ML-Systems/mosml.ML src/Pure/ML-Systems/polyml-5.0.ML src/Pure/ML-Systems/polyml-5.1.ML src/Pure/ML-Systems/polyml-experimental.ML src/Pure/ML-Systems/polyml.ML src/Pure/ML-Systems/smlnj.ML

2009-06-04 wenzelm [Thu, 04 Jun 2009 17:31:37 +0200] rev 31426
tuned signature;
src/Pure/ML/ml_lex.ML

2009-06-04 wenzelm [Thu, 04 Jun 2009 17:31:37 +0200] rev 31425
export esc;
src/Pure/General/symbol.ML

2009-06-04 wenzelm [Thu, 04 Jun 2009 17:31:37 +0200] rev 31424
export value;
src/Pure/General/position.ML