src/Pure/ML/ml_parse.ML
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Thu, 23 Aug 2012 17:46:03 +0200 wenzelm tuned messages: end-of-input rarely means physical end-of-file from the past;
Sat, 23 Jul 2011 17:22:28 +0200 wenzelm explicit structure ML_System;
Sat, 23 Jul 2011 16:37:17 +0200 wenzelm defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
Tue, 24 Mar 2009 11:39:25 +0100 wenzelm eliminated non-canonical alias structure T = ML_Lex;
Mon, 23 Mar 2009 21:40:11 +0100 wenzelm more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
Sun, 22 Mar 2009 19:10:59 +0100 wenzelm ML_Lex.pos_of: regular position;
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Sat, 09 Aug 2008 22:43:59 +0200 wenzelm renamed ML_Lex.val_of to content_of;
Sun, 16 Sep 2007 14:52:28 +0200 wenzelm Minimal parsing for SML -- fixing integer numerals.
less more (0) tip