Sat, 09 Aug 2008 22:43:58 +0200 unified Args.T with OuterLex.token, renamed some operations;
wenzelm [Sat, 09 Aug 2008 22:43:58 +0200] rev 27816
unified Args.T with OuterLex.token, renamed some operations; moved thm_sel to attrib.ML;
Sat, 09 Aug 2008 22:43:57 +0200 unified Args.T with OuterLex.token;
wenzelm [Sat, 09 Aug 2008 22:43:57 +0200] rev 27815
unified Args.T with OuterLex.token; RESET_VALUE of primitive parsers; export keyword_with; renamed keyword_sid to keyword_ident_or_symbolic; added int (from args.ML); added enum(1)', and_list(1)' (formerly in args.ML); removed obsolete arguments/generic_args1 (cf. parse/parse1 in args.ML);
Sat, 09 Aug 2008 22:43:56 +0200 unified Args.T with OuterLex.token;
wenzelm [Sat, 09 Aug 2008 22:43:56 +0200] rev 27814
unified Args.T with OuterLex.token; renamed val_of to content_of; added InternalValue kind; added datatype value/slot with static binding (from args.ML); renamed is_sid to ident_or_symbolic;
Sat, 09 Aug 2008 22:43:55 +0200 unified Args.T with OuterLex.token, renamed some operations;
wenzelm [Sat, 09 Aug 2008 22:43:55 +0200] rev 27813
unified Args.T with OuterLex.token, renamed some operations; removed obsolete parse_args (cf. parse);
Sat, 09 Aug 2008 22:43:54 +0200 unified Args.T with OuterLex.token, renamed some operations;
wenzelm [Sat, 09 Aug 2008 22:43:54 +0200] rev 27812
unified Args.T with OuterLex.token, renamed some operations; unified version of thm_sel (formerly in args.ML and spec_parse.ML);
Sat, 09 Aug 2008 22:43:53 +0200 unified Args.T with OuterLex.token;
wenzelm [Sat, 09 Aug 2008 22:43:53 +0200] rev 27811
unified Args.T with OuterLex.token; moved datatype value/slot and basic operations to outer_lex.ML; removed unused terminator; removed obsolete !!!, position, nat, int, list(1), enum(1) and_list(1) (cf. outer_parse.ML); removed obsolete thm_sel (cf. attrib.ML); one unified version of parse/parse1 (formerly arguments/generic_args1 in outer_parse.ML);
Sat, 09 Aug 2008 22:43:52 +0200 load args.ML later (after outer_parse.ML);
wenzelm [Sat, 09 Aug 2008 22:43:52 +0200] rev 27810
load args.ML later (after outer_parse.ML);
Sat, 09 Aug 2008 22:43:46 +0200 unified Args.T with OuterLex.token, renamed some operations;
wenzelm [Sat, 09 Aug 2008 22:43:46 +0200] rev 27809
unified Args.T with OuterLex.token, renamed some operations;
Sat, 09 Aug 2008 12:28:13 +0200 read_asts: report literal tokens;
wenzelm [Sat, 09 Aug 2008 12:28:13 +0200] rev 27808
read_asts: report literal tokens;
Sat, 09 Aug 2008 12:28:12 +0200 tuned error message;
wenzelm [Sat, 09 Aug 2008 12:28:12 +0200] rev 27807
tuned error message;
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip