Thu, 04 Jun 2009 22:01:54 +0200retrieve ML source files;
wenzelm [Thu, 04 Jun 2009 22:01:54 +0200] rev 31440
retrieve ML source files;

Thu, 04 Jun 2009 19:15:57 +0200export file_name;
wenzelm [Thu, 04 Jun 2009 19:15:57 +0200] rev 31439
export file_name;

Thu, 04 Jun 2009 19:15:55 +0200more robust treatment of bootstrap source positions;
wenzelm [Thu, 04 Jun 2009 19:15:55 +0200] rev 31438
more robust treatment of bootstrap source positions;

Thu, 04 Jun 2009 19:15:54 +0200less experimental polyml-5.3;
wenzelm [Thu, 04 Jun 2009 19:15:54 +0200] rev 31437
less experimental polyml-5.3;

Thu, 04 Jun 2009 18:00:47 +0200just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;
wenzelm [Thu, 04 Jun 2009 18:00:47 +0200] rev 31436
just one ROOT.ML without any cd or ".." -- simplifies ML environment references to bootstrap sources;

Thu, 04 Jun 2009 17:31:39 +0200exn_message/raised: ML_Compiler.exception_position;
wenzelm [Thu, 04 Jun 2009 17:31:39 +0200] rev 31435
exn_message/raised: ML_Compiler.exception_position;

Thu, 04 Jun 2009 17:31:39 +0200eliminated costly registration of tokens;
wenzelm [Thu, 04 Jun 2009 17:31:39 +0200] rev 31434
eliminated costly registration of tokens;

Thu, 04 Jun 2009 17:31:38 +0200convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
wenzelm [Thu, 04 Jun 2009 17:31:38 +0200] rev 31433
convert explicitly between Position.T/PolyML.location, without costly registration of tokens;
added exception_position;

Thu, 04 Jun 2009 17:31:38 +0200added exception_position (dummy);
wenzelm [Thu, 04 Jun 2009 17:31:38 +0200] rev 31432
added exception_position (dummy);

Thu, 04 Jun 2009 17:31:38 +0200reraise exceptions to preserve original position (ML system specific);
wenzelm [Thu, 04 Jun 2009 17:31:38 +0200] rev 31431
reraise exceptions to preserve original position (ML system specific);